A mathematical proof consists of a sequence of reasoning that leads to a certain conclusion. Lean, a programming language created in 2013 by Leonardo de Moura, from Rio de Janeiro, allows for the verification of these proofs to identify flaws or errors.
In September, Lean became a focal point of controversy after OpenAI, the company behind ChatGPT, announced a solution to the Navier-Stokes mathematical problem, one of the Millennium Prize Problems, whose solutions are valued at US$1 million each. The scientific community debates whether this demonstration truly addresses the original question, although it is a fact that it is logically perfect, something that Lean ensures.
This possibility was unthinkable both in 2023 and in 2013. The author reports that he worked at Microsoft, where theorem provers were employed to ensure that software was free of bugs. However, this method was ten times more expensive than developing the program internally, limiting its use to critical sectors, such as cryptography. No one anticipated that Fields Medalists, like Terence Tao, would start using this system. Currently, when someone contacts Tao claiming to have proven a conjecture, his response is: 'Check it first in Lean.'
Many mathematicians were unaware of Lean's existence and raise pertinent questions, such as whether it has flaws or if it can be trusted. In the specific case of Navier-Stokes, which contains hundreds of thousands of lines written in Lean, community members examined the proof using verifiers they themselves created, and it was approved. Thus, the crisis of confidence resides more in ethical issues, such as allegations that AI companies consume excessive water or steal data. Although these are relevant topics, they cannot halt the advancement of mathematics.
There are varied reactions: some show enthusiasm, others feel fear of becoming obsolete, and some believe that artificial intelligence will annihilate mathematics. Peter Scholze, considered one of the greatest living mathematicians, declared that he would die without using AI. On the other hand, Kevin Buzzard had planned a five-year project to formalize Fermat's Last Theorem in Lean. In April, he laughed when asked if AI would help; months later, it completed the work in just 11 days. The author concludes that many are experiencing a 'mourning,' comparing the reaction of those who did mental calculations to the advent of the calculator, which, despite initial resistance, benefited humanity. He learned not to challenge AI.