Mathematicians hope digital "proof assistants" will fix the field's own replication crisis

Computer programs can be better than humans, but they're not perfect

Spread the knowledge

 Max Duzij / Unsplash 

While it’s tempting to think that math is a discipline free from mistakes, the reality is quite different.  Published proofs have been found to contain errors and, worryingly, modern proofs are sometimes so long and complicated that it’s difficult for mathematicians to check that they are correct. (A proof, in mathematics, is a step-by-step logical argument that asserts some conclusion about a mathematical statement.) 

In a recent article published in the journal The Mathematics Intelligencer, Cambridge mathematician Anthony Bordg compared this situation to the replication crisis in science. According to his analogy, attempts to check the correctness of a proof are like attempts to replicate a scientific experiment.  If everything is correct, the proof has been replicated.  But if an error is found or if mathematicians cannot determine whether the proof is correct for some other reason, then the attempt to replicate the proof has failed. 

But too many proofs cannot be replicated.  So, what can we do to fix this?

One potential solution is to use computers during the peer review process.  Software called proof assistants can check if a proof is correct, once the proof has been translated into a language the software understands.  While human reviewers do not always rigorously check that every single inference in a proof is correct, a proof assistant does. And if it finds anything amiss, it will complain. A proof assistant's blessing therefore counts as a successful replication of the proof “once and for all.” 

But mathematicians have not yet welcomed proof assistants with open arms.  One problem is that they are not exactly user friendly, and Bordg acknowledges that there is plenty of room for improvement.  With further development, proof assistants will hopefully become more widely used in the near future.