A group of mathematicians discovered an error in an important 60-year-old proof. The error has been corrected. However, this case highlights the possibility that other errors are lurking in the mathematical literature.
An error in a proof underlying a widely used branch of modern mathematics was discovered accidentally by mathematicians while translating ancient proofs into a computer language.
The error was quickly corrected, but this is an episode that highlights the importance of making mathematics computer-readable to detect other possible examples.
As , most modern mathematics resides in research papers and textbooks, and depends on the fact that mathematicians check each other’s work to make sure it is correct.
Recently, researchers at Imperial College London began an ambitious project to formalize the proof of Fermat’s last theorem – very important in modern mathematics.
The proof in question here employs many different cutting-edge branches of the discipline, many of which are not yet machine-readable so need to be translated first.
One of them is a part of geometry called crystal cohomology.
While working on the translation, the mathematician Antoine Chambert-Loirfrom Paris Cité University, came across an error: A section of an old proof that forms the basis of crystalline cohomology, written in an article by the French mathematician Norbert Roby em 1965appeared to contain an error.
Upon closer inspection, Chambert-Loir discovered that Roby appeared to have forgotten a symbol between one line and another, invalidating the proof.
But calm down…
After the researchers discussed the error, Brian Conrad of Stanford University in California found proof for what Roby was trying to prove, showing that despite everything, Roby’s mistake was not fatal.
This makes this particular problem a relatively small problem, but still a potential harbinger of larger, unknown errors that may be lurking in the mathematical literature.
To New Scientist, Chris Birkbeck from the University of East Anglia, in the United Kingdom, points out how surprising it is that a domain as widely used as crystal cohomology originally depended on references so obscure and difficult to find.
The expert clarifies that formalizing mathematics will now help verify that the mountain of academic literature that currently exists no longer contains errors: “Mathematics is becoming quite complicated. It’s impossible to go and read everything up to the axiom [as verdades aceites da disciplina]”.
“The idea that a fundamental result could contain an error, which was then used in thousands of subsequent works, is a nightmare”, said Chris Williams, from the University of Nottingham, in the United Kingdom, to the same magazine.
