It would take 10 billion years for a human being to read it. With its phenomenal size of 200 terabytes—the equivalent of all of the digital texts held by the Library of Congress—it is the longest mathematical proof ever produced. Three American-British computer scientists have just announced its creation using a supercalculator.1 Their work was presented during the SAT international conference, which took place in Bordeaux July 5-8 of this year.

A 30-year-old problem solved in force

The problem that the three researchers solved, and that required such a long proof, is known as the "Boolean Pythagorean triples problem." Remaining unsolved since the 1980s, this seemingly simple problem posits the following question: is it possible to color each positive integer blue or red in such a way so that no integer triplet (a, b, and c) that satisfies the famous Pythagorean equation (a² + b² = c²) is entirely the same color? For example, for the triplet 3, 4, and 5, if 3 and 5 are colored blue, then 4 must be red.

The trio of computer scientists gave their answer: no. They showed that up until 7,824, it is possible to color integers in this way, even doing so in multiple ways, however beginning with 7,825, it becomes impossible. "To prove it, the researchers had to proceed 'in force' by listing and verifying an incredible number of possible combinations," explains Laurent Simon of the LaBRI.2

Grid showing one of the solutions for the Boolean Pythagorean triples problem for numbers 1 to 7,824.

Grid showing one of the solutions for the Boolean Pythagorean triples problem for numbers 1 to 7,824.

MARIJN HEULE

MARIJN HEULE

Share

Share

Humans not need apply

A task beyond the reach of humans, but accessible for a computer. Just consider that there are more than 10²³⁰⁰ ways of coloring the integers up until 7,825! Fortunately, by taking advantage of the different symmetries of the problem and by using various techniques from number theory, the researchers were able to reduce the number of possibilities to be studied to 1 trillion. "The team cleverly chopped up all of these possible cases in a million different parcels in order to solve the problem more easily," points out Daniel Le Berre of CRIL.3

It took two days and only 800 of the many processors of the Stampede supercalculator at the University of Texas to review all of these possibilities and provide the long-awaited proof, generating 200 terabytes in the process. "The researchers then verified the proof, which is too long to be read by a human, by using another independent software program," Simon adds.

Computers have now become indispensable allies for mathematicians in resolving this type of combinatorial problem. Already in 2014, computers were used to build a proof measuring 13 gigabytes—the previous record—that made it possible to end an enigma similar to that of Pythagorean triples.

The SAT solving revolution

What made this little revolution possible? The development of highly effective new algorithms by computer scientists to solve these problems, known as "SAT solvers." In IT language, SAT means "satisfiability," and involves a logical formalism that captures all of the difficulty of a combinatorial problem in order to then try to satisfy it. A game of Sudoku or minesweeper are two very simple examples of problems that can be grasped and resolved very easily by this formalism.

In 1976, 1,200 hours of calculations on a computer were needed to demonstrate the validity of a theorem stating that 4 colors were enough to color a map without any adjacent area being the same color.

In 1976, 1,200 hours of calculations on a computer were needed to demonstrate the validity of a theorem stating that 4 colors were enough to color a map without any adjacent area being the same color.

FIBONACCI/COMMONS WIKIMEDIA/CC BY-SA 3.0

FIBONACCI/COMMONS WIKIMEDIA/CC BY-SA 3.0

Share

Share

In fifteen years, computer engineers have made considerable progress in this area. "So much so that SAT solvers, which were initially confined to theoretical computer science, have seen their use explode, and have made it possible to solve increasingly difficult problems," reveals Le Berre. Today Microsoft uses these algorithms to test the device drivers of its new operating systems by identifying from among millions of series of instructions those that could cause a bug in the software, or by proving on the contrary that there are no such series. The same is true for Intel, which uses these tools to verify the proper functioning of its microprocessors. And the number of applications continues to grow in robotics, bioinformatics, and cryptography.

Others proofs to come...

Today it is the turn of mathematics to be affected by this wave. For instance, in order to establish the proof for the Boolean Pythagorean triples problem, the trio of computer scientists used the solver called Glucose, developed by Laurent Simon and Gilles Audemard from the CRIL. In 2014, it was again Glucose that made it possible to create what was the longest mathematical proof at the time.

And this trend is likely to continue. "This latest result shows that it is possible to use this method to tackle extremely difficult combinatorial mathematical problems, for which no classical approach by hand is available yet," adds Simon. "It probably prefigures the end of other similar conjectures that still resist mathematicians today."