Verifying that a mathematical proof is correct

Thomas Hales had submitted a proof in 1998. After four years of work the referees reported that they were ninety nine percent certain it was right and could go no further, which is an honest account of the limits of human checking on a long computational argument. Hales then spent a decade making the proof readable by a machine instead. Since then the Lean assistant has absorbed large tracts of modern mathematics, and Kevin Buzzard began a five year effort in 2024 to formalise Fermat's Last Theorem. What is contested is the certifying step, where a proof assistant is now more reliable than a tired referee, while deciding that a statement is worth proving, that an argument explains something, and that a paper should appear, remain acts of judgment nobody has proposed to hand over.