Uma prova matemática consiste em uma sequência de raciocínios que conduz a uma conclusão certa. O Lean, uma linguagem de programação criada em 2013 por Leonardo de Moura, oriundo do Rio de Janeiro, possibilita a verificação dessas provas para identificar falhas ou erros.
Em setembro, o Lean tornou-se um ponto focal de controvérsia após a OpenAI, empresa proprietária do ChatGPT, anunciar uma solução para o problema matemático de Navier-Stokes, um dos Sete Problemas do Milênio, cujas soluções são avaliadas em US$ 1 milhão cada. A comunidade científica debate se essa demonstração realmente aborda a questão original, embora seja um fato que ela é logicamente perfeita, algo que o Lean assegura.
Essa possibilidade era impensável tanto em 2023 quanto em 2013. O autor relata que trabalhava na Microsoft, onde provadores de teoremas eram empregados para garantir que softwares estivessem livres de falhas. Contudo, esse método era dez vezes mais caro do que desenvolver o programa internamente, limitando seu uso a setores críticos, como a criptografia. Ninguém antecipou que medalhistas Fields, como Terence Tao, passariam a utilizar este sistema. Atualmente, quando alguém contata Tao alegando ter comprovado uma conjectura, sua resposta é: «Verifique primeiro no Lean».
Muitos matemáticos desconheciam a existência do Lean e levantam questionamentos pertinentes, como se ele possui falhas ou se pode ser confiável. No caso específico de Navier-Stokes, que contém centenas de milhares de linhas escritas em Lean, os membros da comunidade examinaram a prova utilizando verificadores que eles próprios criaram, e ela foi aprovada. Assim, a crise de confiança reside mais em questões éticas, como alegações de que empresas de IA consomem excesso de água ou furtam dados. Embora sejam temas relevantes, estes não podem deter o avanço da matemática.
Existem reações variadas: alguns demonstram entusiasmo, outros sentem receio de se tornarem obsoletos, e há quem acredite que a inteligência artificial irá aniquilar a matemática. Peter Scholze, considerado um dos maiores matemáticos vivos, declarou que morreria sem utilizar IA. Por outro lado, Kevin Buzzard havia planejado um projeto de cinco anos para formalizar o Último Teorema de Fermat no Lean. Em abril, ele riu quando lhe perguntaram se a IA auxiliaria; meses depois, ela realizou o trabalho em apenas 11 dias. O autor conclui que muitos estão vivenciando um «luto», comparando a reação daqueles que faziam cálculos mentais ao surgimento da calculadora, que, apesar da resistência inicial, beneficiou a humanidade. Ele aprendeu a não desafiar a IA.
