In a column in Folha, Viana talks about the future of mathematics after AI
Reproduction of Marcelo Viana’s column in Folha.
How do you arrange cannonballs in a ship’s hold in such a way that as many as possible fit? This practical concern of the British navy gave rise to the mathematical problem of ball packing, first formulated in 1611 by Johannes Kepler: which arrangement of (identical) balls can hold the most balls per unit volume?
Kepler believed that the answer would be hexagonal packing in layers, which is precisely the way oranges are usually displayed at the fair. But he couldn’t prove it, and there was virtually no progress until the middle of the 20th century.
In 1953, the Hungarian László Tóth reduced the problem to a finite (but enormous!) number of calculations. In 1998, the American Thomas Hales announced that he had completed these calculations. But his paper was too long (250 pages plus 3 gigabytes of code): the experts responsible for reviewing it threw in the towel after four years of work.
To put an end to the doubts, the following year Hales launched the Flyspeck project: for more than a decade, a team of mathematicians transcribed all the steps of the proof into a formal language, so that they could be rigorously checked by computer. The work was only finished in 2014, but it was conclusive: the reasoning is correct and therefore the problem of packing spheres in dimension 3 has been definitively solved.
Mathematically, the problem makes sense in any dimension and, curiously, the next breakthroughs came in high dimensions.
In 2016, Ukrainian Maryna Viazovska used a specific property of dimension 8 to solve the question in that dimension. Soon after, together with collaborators, she extended the proof to dimension 24. These are impressive feats, combining sophisticated ideas from number theory, discrete geometry and harmonic analysis. For these results, Viazovska won the Fields medal in 2022. The problem remains open in all other dimensions greater than 3.
Now, the startup Math Inc. has just announced that a team led by Viazovska herself has managed to transcribe the proof of these results into Lean language, making them the first “Fields medal” theorems to have their proofs formally verified by a computer. And one of the protagonists of this project is Gauss, the artificial intelligence specialized in automatic formalization at Math. Inc.
After dealing with various auxiliary results, Gauss transcribed Viazovska’s theorem in dimension 8 for Lean in just 5 days. Then, in the space of two weeks, he dealt with the dimension 24 case, using only the original article as a basis and carrying out bibliographic research independently when necessary. In total, Gauss generated 200,000 lines of Lean code (MathLib, the worldwide Lean repository, currently has around 2 million lines), containing many other relevant results.