Folha: ‘The liquid tensor experiment’
Reproduction of Marcelo Viana’s column in Folha.
The German Peter Scholze, who won the Fields medal, the most important prize in mathematics, here in Rio de Janeiro in 2018 at the age of just 31 (!), is widely considered to be one of the most brilliant mathematicians of our time. But in 2020 he was in a delicate situation: one of his main theorems, a key part of his theory of liquid vector spaces, had a proof so subtle and intricate that neither the reviewers nor Scholze himself could be sure it was right.
His reaction was unusual: in December of that year, Scholze published an open invitation to the scientific community to have his proof formally verified by computer. He even offered a prize for the verification, adding that he would be very relieved if it could be done. A group of experts responded to the challenge, launching what became known as the “liquid tensor experiment”.
The most widely used tool for formally checking mathematical arguments is the Lean programming language, created in 2013 by Leonardo de Moura, a Brazilian researcher at Microsoft Research. It was originally conceived as a means of automatically checking computer programs, i.e. detecting possible “bugs” (errors) directly in the code without having to run the program.
It turns out that a computer program and a mathematical proof are essentially the same thing. This is a principle of computer science that even has a name: Curry-Howard correspondence, in honor of the American researchers Haskell Curry (1900 – 1982) and William Howard (b. 1926). Lean has also become a means of automatically detecting errors in mathematical reasoning.
To simplify things a little, the idea is to transcribe the reasoning into Lean language and then make the computer run the code obtained in this way. Lean acts as a relentless and infallible proofreader, which doesn’t miss the slightest logical error. If the code runs to the end, the proof is formally correct.
This is what the liquid tensor experiment group did for Scholze’s theorem. Thus, by June 2021, they had managed to validate the most difficult step of the proof, leading Quanta Magazine, one of the best science magazines today, to proclaim that “the proof checkers have entered the first division of mathematics”. The group’s work was officially completed a year later, with complete success: Scholze’s arguments were fully validated.
It was the first time that a theorem at the frontier of knowledge had its proof formally validated in this way. And the fact that the author himself, a mathematician of Scholze’s level, acknowledged his insecurity about the proof gave the project a special dimension, pointing out that computer assistants have become important tools in mathematical research, even when carried out by humans.