07/08/2018

'Every mathematical proof must be understandable and verifiable'

It doesn't matter if it's a map of Brazil, with its 26 states (and one Federal District), or the giant USA, which boasts 50 federative units. According to mathematicians, any map, real or imaginary, can be colored with just four colors, so that neighboring regions don't have the same color.

Although traditionally considered the landmark birth of the field of machine-assisted proof, the "Four-Color Map Theorem," proven by Appel, Haken, and Koch in 1976, was not the first formulation verified by machine. More than ten years earlier, theorems were already being proven through exhaustive enumerations on computers.

At the International Mathematical Union (IMU) panel, experts in machine-assisted proof gathered to discuss the implications of this type of mathematical proof (at least partially computer-generated) for authors, publishers, and readers. Moderated by James Davenport, the roundtable included mathematicians Bjorn Poonen, James Maynard, Harald Helfgott, Pham Huu Tiep, and Luís Cruz-Filipe.

To date, most machine-assisted proofs have been implementations of large proofs by exhaustion of a mathematical theorem. The idea is to use a computer program to perform lengthy calculations and provide a proof that the result of these computations implies the given theorem.

However, the method is the subject of controversy in the world of mathematics. The difficulty of verifying proofs with many logical steps and the fact that computational processes can be affected by program errors or defects in runtime and hardware are some of the arguments raised.

"It doesn't matter if the evidence was created by a computer or by a human; all of them have to be understandable and verifiable," Poonen emphasized.