Em 6 de outubro de 2026, a OpenAI publicou o anúncio “Sharing AI progress in mathematics”, com uma série de novos resultados matemáticos produzidos por um modelo interno, que ainda não foi lançado ao público.
O que foi divulgado
- Os resultados foram publicados em um repositório no GitHub (openai/math), em vez de uma revista científica tradicional.
- Muitas das provas vêm acompanhadas de formalizações em Lean, uma linguagem que permite que um computador verifique se a demonstração está correta.
- Em média, cada resultado usou o equivalente a cerca de três horas de raciocínio do ChatGPT Pro.
- A abordagem foi discutida com um grupo consultivo do Institute for Advanced Study (IAS), de Princeton.
A repercussão
O anúncio movimentou a comunidade matemática. O cientista da computação Scott Aaronson contou em seu blog que o pacote reúne 372 resultados e inclui uma prova da Conjectura dos Jogos Únicos, de Subhash Khot, um problema famoso da teoria da computação, acompanhada de um certificado em Lean. Ele mesmo pondera que a análise humana dessas provas mal começou.
As ressalvas
- Nem todas as provas foram formalizadas ainda; a OpenAI diz que vai adicionar mais.
- O modelo usado é interno, e a empresa diz que trabalha para lançá-lo de forma responsável.
- A OpenAI promete financiar workshops e conferências para ajudar os matemáticos a analisar resultados produzidos por IA.
Minha opinião: matemática é uma das áreas em que dá para checar se a IA acertou, e o uso do Lean é o que torna isso confiável. Se esses resultados se confirmarem, pode ser um marco. Mas vale esperar a avaliação dos especialistas antes de comemorar.