Brasileiro cria linguagem que valida revolução na matemática por IA

Uma prova matemática consiste em uma sequência de argumentos capaz de conduzir, gradualmente, a uma conclusão inevitável. Desenvolvido em 2013 pelo carioca Leonardo de Moura, o Lean atua como uma linguagem de programação voltada para inspecionar essas demonstrações, identificando eventuais lacunas e deslizes lógicos.

Em setembro, a ferramenta assumiu o centro de uma grande polêmica quando a OpenAI, criadora do ChatGPT, revelou uma solução para o problema matemático de Navier-Stokes, integrante dos chamados Problemas do Milênio, cujos prêmios chegam a US$ 1 milhão cada. Embora a comunidade acadêmica ainda debata se a demonstração de fato soluciona a indagação inicial, é inegável que sua lógica é irrepreensível — um respaldo garantido pelo Lean.

O que é “vibe coding”?

Você imaginava que o Lean seria útil para lidar com IAs? Ninguém imaginava isso nem em 2023, muito menos em 2013. Eu estava na Microsoft, onde se usam provadores de teoremas para mostrar que um software não tem bugs. Mas isso custava dez vezes mais do que construir o próprio programa, então só valia a pena em áreas críticas, como criptografia. Nunca imaginamos que medalhistas Fields (o “Nobel da matemática”) como Terence Tao usariam o sistema. Hoje, quando alguém escreve ao Tao dizendo ter provado uma conjectura, ele responde: “Cheque no Lean primeiro”.

Por que ainda há tanta desconfiança em relação à prova da OpenAI? Muitos matemáticos nem sabiam que o Lean existia, e fazem perguntas válidas: ele tem bugs? Posso confiar? No caso de Navier-Stokes, que tem centenas de milhares de linhas em Lean, membros da comunidade checaram a prova com verificadores que eles mesmos construíram, e ela passou. Então, a crise de confiança está mais no nível ético, em acusações como a de que empresas de IA gastam água demais e roubam dados. São questões importantes, mas não dá para parar a revolução na matemática.

Como a comunidade matemática está reagindo à ascensão da IA? Tem gente animada, gente com medo de ficar obsoleta, gente que acha que a IA vai destruir a matemática. O Peter Scholze, um dos maiores matemáticos vivos, jurou que vai morrer sem usar IA. Já o Kevin Buzzard tinha um projeto de cinco anos para formalizar o Último Teorema de Fermat no Lean. Em abril, ele riu quando perguntaram se a IA ajudaria. Meses depois, ela fez o trabalho em 11 dias. Acho que muitos estão passando por um “luto”. Quem fazia contas de cabeça deve ter ficado chateado quando inventaram a calculadora, mas ela foi um bem para a humanidade. Aprendi a não apostar contra a IA.