An error in a proof underlying a widely used branch of modern mathematics was accidentally discovered by mathematicians while translating old proofs to a computer language. The mistake was swiftly fixed, but mathematicians say that the episode highlights the importance of making maths computer-readable to catch other possible examples.
Most modern mathematics resides in research papers and textbooks, and relies on mathematicians checking each other’s work to make sure it is correct. A proof is essentially a social construct – if enough mathematicians are satisfied that the logical steps of a proof are correct, then it is considered true. On the rare occasions this process goes wrong, a proof can be left in limbo.
One way to avoid this is to have proofs checked step-by-step using a computer, but doing so involves translating them into computer-readable languages in a process called formalisation. This is a relatively new idea, and can be time-consuming.
Advertisement
Recently, at Imperial College London and his colleagues began an ambitious project to formalise the proof of Fermat’s last theorem, which is important in modern maths. The proof employs many different cutting-edge branches of the subject, much of which isn’t yet machine-readable, so these must be translated first.
One of these is a part of geometry called crystalline cohomology. While working on translating this, at Paris Cité University encountered an error. A section of an old proof that forms the foundations of crystalline cohomology, written in a paper by French mathematician Norbert Roby in 1965, appeared to contain a mistake. On closer inspection, Chambert-Loir found that Roby appeared to have forgotten a symbol between one line and another, invalidating the proof.
This would be a major problem for mathematicians, wrecking many more recent proofs, if Roby’s work was the only evidence for crystalline cohomology being correct, says Buzzard, but it is so widely used and has been proven using so many different strategies since, that it was incredibly unlikely the proof couldn’t be fixed.
After Buzzard discussed the error with colleagues, at Stanford University in California, found a separate, later proof for what Roby was trying to prove, showing that Roby’s error wasn’t fatal after all. That makes this particular problem a fairly small one, but still a potential harbinger of larger, unknown errors that may be lurking in the mathematical literature.
It is surprising that such a widely used field as crystalline cohomology was originally dependent on such obscure and hard-to-find references, says at the University of East Anglia in the UK, but formalising mathematics will help verify that the mountain of academic literature that now exists doesn’t contain more mistakes. “Maths is getting quite complicated. It’s impossible to go through and read every single thing down to the axiom [the subject’s accepted truths],” he says.
“The idea that a foundational result may contain an error, that has then been used in thousands of subsequent works, is a nightmarish one,” says at the University of Nottingham, UK. “Formalisation seems to give another lock on the validity of the foundations on our field that is very welcome.”
