Folha: ‘Lean, a new math showdown’

Reproduction of Marcelo Viana’s column in Folha de S. Paulo.

One thing that has always attracted me to mathematics is that it is the only field of knowledge in which it is possible to give definitive answers to virtually any question: when a mathematician proves (or “disproves”) a theorem, that debate is over and we simply move on to new questions.

In theory, at least. In practice, as I commented here recently, in some cases the proof is so complex and subtle that it’s hard to be sure whether it’s correct or not. And this problem is getting worse as mathematical works become longer and more sophisticated. Fortunately, advanced computational tools are entering the field to help, and we are beginning to glimpse the possibility that they will end up doing this job for us. Their advocates go further, predicting that they will soon change the way we discover new mathematical results.

The most popular of these tools is Lean, a programming language and theorem checker developed at Microsoft Research in 2013 by the team of Brazilian Leonardo de Moura, who has a PhD in computer science from PUC-Rio. An important feature is that Lean is interactive, it presupposes collaboration between the mathematician and the computer. It works more or less like this.

The mathematician formulates the theorem he wants to prove: this is his Goal. He then writes short commands, such as “simplify”, “rewrite”, “apply”, etc. Each time, Lean responds by stating the assumptions behind the command and which of them still need to be proved, leaving no gaps in the logic. In this way, the Objective is broken down into simpler steps, until all of them have been duly justified. At this point, Lean declares that the Goal has been achieved: the veracity of the evidence has been formally proven.

This kind of approach would be unfeasible if, each time, all the steps had to be justified again from the basic axioms of mathematics. Instead, Lean collects a large “library” (repository) of theorems that have already been formally verified and can therefore be invoked directly in the proof of new theorems. MathlLib, as it is called, already contains hundreds of thousands of theorems, formulated in more than 2 million lines of Lean code.

It may sound easy, but it isn’t: validating a significant theorem in Lean is laborious and time-consuming. But for some of today’s leading experts, it’s a strategic opportunity for mathematics, with enormous potential for impacting the future of the discipline. Among the biggest advocates is none other than Terence Tao, winner of the Fields Medal in 2006, who even developed his own proof-checking tool to assist him in his research.

To read it in full, visit Folha’s website.