Catswatch

Has mathematics become an experimental science? Yes, according to the most prestigious journal of mathematics-at least that part of maths that involves computer proofs. It seems that some of the most famous problems in maths can only be solved with the assistance of computers, and the computer parts of these proofs are essentially uncheck able and should instead be thought of as similar to scientific experiments.

Whatever happened to the cut and dried world of maths, where either a mathematical theorem has been proved or it hasn’t? Up until recently it was obvious what a mathematical proof should look like- a rigorous argument, consisting of a sequence of logical steps written on paper that any expert in the field could read, understand and believe.

Over the last 30 years a new breed of proof has emerged; one which relies on a computer to carry out of the work alongside a more traditional mathematical argument. One of the most famous computer proofs is for the deceptively simple Four Colour Theorem, which states that four colours is enough to colour any map without having to use the same colour any map without having to use the same colour for any two adjacent countries. Originally conjectured in 1852, this theorem was finally proved in 1976 by Kenneth Appel and Wolfgang Haken. Their proof relied on a computer to check a large number of special cases. Some mathematicians thought that using a computer was cheating.

It was important to accept computer proofs in order to expand the type of mathematics that was publishable. The most compelling reason was that “there are interesting theorems that can only be proved using computers.”

The final decision is that Annals will publish the theoretical part of the proof, which has been checked successfully, but the computer section will be published separately in a more specialized journal. This was a disappointing outcome to what had seemed like a promising step towards gaining greater acceptance of computer proofs in mathematics.

But perhaps it is not so surprising that proofs of such a different nature will need to be assessed very differently. Annals has amended its policy on computer proofs, and will not now expect to verify the computer sections of proofs to the same through standard as it will continue to apply to the theoretical parts. Instead, computer proofs will be treated as more akin to experiments, which are accepted by referees if certain standards are met and consistency checks are satisfied.

Who knows how computers may enhance mathematicians’ vision in the future? But many will have been drawn to the subject in the first place by the concrete nature and beauty of a written proof. And those mathematicians may never be truly satisfied with a proof that no human can hope to understand.
Portugues | Francais | Espanol | Deutsche | Italiano | Chinese | Korean | Japanese