There are (short) computer programs where you input a mathematical proposition and a proof in a kind of proof programming language, and the program will then check if it's a valid proof. Saying that mathematical truth is a social construct is technically true but misses the point entirely.