IA da OpenAI usa Lean para prova matemática de US$ 1 milhão

A OpenAI, empresa por trás do ChatGPT, anunciou recentemente uma solução para o problema matemático de Navier-Stokes, um dos sete Problemas do Milênio, que oferece um prêmio de US$ 1 milhão. A prova foi desenvolvida e verificada utilizando o Lean, uma linguagem de programação e sistema de verificação de provas criado em 2013 pelo brasileiro Leonardo de Moura. A ferramenta é projetada para garantir a correção lógica de demonstrações matemáticas, identificando lacunas e erros.

O uso do Lean na verificação da prova da OpenAI gerou discussões na comunidade matemática. Embora a ferramenta assegure a correção lógica da demonstração, que possui centenas de milhares de linhas em Lean, a validade da solução para a questão original de Navier-Stokes ainda é debatida. Membros da comunidade matemática confirmaram que a prova passou pelos verificadores do Lean, construídos por eles mesmos, o que solidifica a confiança na integridade lógica do trabalho.

O que é o Lean e como ele funciona?

Criado originalmente para verificar a correção de softwares em áreas críticas como criptografia, o Lean se tornou uma ferramenta poderosa para a matemática pura. Ele permite que matemáticos formalizem suas provas, transformando-as em um formato que pode ser rigorosamente checado por um computador. Isso elimina a possibilidade de deslizes lógicos ou lacunas argumentativas que poderiam passar despercebidas em revisões humanas tradicionais.

O criador do Lean, Leonardo de Moura, que trabalhava na Microsoft na época, não imaginava que a ferramenta seria utilizada por matemáticos de renome mundial, como Terence Tao, medalhista Fields. Atualmente, é comum que matemáticos peçam para que conjecturas sejam verificadas no Lean antes de serem consideradas. A adoção da ferramenta representa uma revolução na forma como as provas matemáticas são construídas e validadas.

A reação da comunidade matemática à IA

A ascensão da inteligência artificial na matemática tem provocado reações diversas entre os pesquisadores. Alguns demonstram entusiasmo com o potencial de novas descobertas e aceleração de processos, enquanto outros expressam receio de que suas habilidades se tornem obsoletas ou que a IA possa, de alguma forma, prejudicar a disciplina. O matemático Peter Scholze, por exemplo, declarou que não usará IA em seu trabalho.

Em contrapartida, Kevin Buzzard, outro matemático proeminente, viu um projeto de cinco anos para formalizar o Último Teorema de Fermat no Lean ser concluído pela IA em apenas 11 dias. Essa experiência ilustra a capacidade da IA de acelerar significativamente tarefas complexas. Moura compara a situação à invenção da calculadora, que, apesar de ter mudado a forma de fazer contas, foi um avanço benéfico para a humanidade. Ele aconselha a não apostar contra a IA.

O que diz a pesquisa

A declaração Leiden Declaration on Artificial Intelligence and Mathematics, publicada como preprint no arXiv em 2026, aborda os desafios impostos pelo uso da inteligência artificial na pesquisa matemática. O documento destaca que as recentes tecnologias de IA, incluindo métodos simbólicos e neurais para geração e formalização de matemática, podem ter iniciado um novo capítulo na história da disciplina. A declaração observa uma gama de reações entre pesquisadores, desde entusiasmo pelo potencial de novas descobertas até preocupação com as implicações para a matemática e a sociedade.

O texto chama os matemáticos a exercerem responsabilidade sobre a adoção da IA em suas pesquisas e fornece recomendações para indivíduos, instituições, governos e indústria. Embora o foco seja a pesquisa matemática, muitas das recomendações se aplicam a outras áreas, como educação, mentoria, publicação, financiamento, política científica e o uso da matemática no mundo.