While it’s tempting to think that math is a discipline free from mistakes, the reality is quite different. Published proofs have been found and, worryingly, modern proofs are sometimes so long and complicated that it’s difficult for mathematicians to . (A proof, in mathematics, is a step-by-step logical argument that asserts some conclusion about a mathematical statement.)
In a published in the journal The Mathematics Intelligencer, Cambridge mathematician Anthony Bordg compared this situation to the . 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 can check if a proof is correct, once the proof has been translated into a language the software understands. While human reviewers do , a proof assistant And if it finds anything amiss, it will complain. A proof assistant's blessing therefore counts as a successful replication of the proof “.”
But mathematicians have not yet welcomed proof assistants with open arms. One problem is that they are not exactly user friendly, and Bordg that there is plenty of room for improvement. With further development, proof assistants will hopefully become more widely used in the near future.