Folha: ‘AI in the formalization of mathematics’

Reproduced from Marcelo Viana’s column in Folha.

Math Inc. (in Brazil it would be“Matemática S.A.”) is a California-based startup dedicated to the formalization of mathematics, i.e. the transcription of definitions and theorems into formal language systems such as Lean, which I talked about here last week.

The company has an extremely ambitious vision (“Those who are paying attention can feel the dawn of a new golden age of mathematics”…), but the most concrete goal is to be able to automatically verify that the reasoning is correct and, therefore, that the theorems have actually been proved with total rigor. To this end, their collaborators include some of today’s best experts, such as Maryna Viazovska and Terence Tao, both Fields Medal winners.

In January 2024, Tao and his colleague Alex Kontorovich proposed to the scientific community to formalize in Lean the theorem of prime numbers, one of the most important results of number theory, proved independently in 1896 by the Frenchman Jacques Hadamard and the Belgian Charles de la Vallée Poussin.

This theorem states, roughly speaking, that the percentage of numbers from 1 to N that are prime is inversely proportional to the number of digits in N. In particular, primes become rarer and rarer as we increase N. The proof uses very deep mathematical ideas, and it was clear from the start that formalizing it would be a highly non-trivial challenge. Kontorovich and Tao worked on the problem for 18 months, with partial progress.

Then, on March 10, Math Inc. announced that it had completed the task using a new artificial intelligence, Gauss, “a pioneering autoformalization agent designed to assist mathematicians in the formal verification of theorems”. According to the company, the agent can work autonomously for hours, without human help, which dramatically speeds up the work.

In just three weeks, Gauss transcribed the proof into around 25,000 lines of Lean code, containing more than a thousand definitions and auxiliary theorems. By way of comparison, the largest project of this kind ever carried out generated 500,000 lines, but took more than a decade (!) to execute. The expectation is that future formalization agents will be increasingly autonomous and fast.

All these codes are now part of MathLib, Lean’s worldwide repository, which already has around 2 million lines, covering 350,000 theorems and definitions. That’s the equivalent of about 50 advanced math textbooks. And this material is available to be invoked in the validation of new theorems, which means that as the formalization project progresses, it should also accelerate.

Math Inc. says it believes this will also make it feasible to train universalist artificial intelligences, mastering all areas of mathematics. Among humans, the last universalists were Henri Poincaré and David Hilbert, a century ago.

Read the full column on the Folha website.