OpenAI: dez resultados matemáticos formalizados em Lean e o papel do modelo interno

A 1 de agosto a OpenAI publicou o manuscrito «Ten Advances in Mathematics and Theoretical Computer Science», atribuindo os resultados a um modelo interno próprio. Ao mesmo tempo foi criado o repositório GitHub `openai/ten-proofs`, que disponibiliza as formalizações em Lean 4 das dez demonstrações. Entre os resultados destacam-se a melhoria do expoente para o empacotamento de esferas — a primeira desde 1978 —, a construção de um grupo não sófico e um contraexemplo à conjetura de rigidez de Connes. O repositório é um projeto Lean 4.32.0 assente em mathlib, publicado com licença Apache-2.0: qualquer pessoa pode recompilar as demonstrações com `lake exe cache get` e `lake build All`, e uma pasta ComparatorChallenges explica como fazer a verificação de forma independente.

As notícias ligaram estes resultados a «Astra», o nome da próxima família de modelos anunciada pela OpenAI nesse mesmo 1 de agosto; o manuscrito, porém, fala apenas de «um modelo interno», não lançado. Dados como o custo de cerca de 2000 dólares em tokens ou as 249 páginas do documento vêm de reportagens de terceiros, uma vez que a página oficial do anúncio está neste momento inacessível. O artigo agradece a matemáticos humanos pela releitura e assinala um trabalho independente e simultâneo de Shuoxing Zhou, desenvolvido em parte com a assistência do GPT-5.6 Sol.

Segundo a SiliconANGLE os argumentos matemáticos vêm do modelo, mas foram investigadores humanos a transformar o resultado em manuscritos publicáveis: quanto pesa esse acabamento não está quantificado. O uso de Lean 4 desloca o debate: o certificado garante a validade lógica da demonstração, mas não confirma automaticamente que o enunciado formalizado coincida com o problema histórico em aberto — controlo que continua a ser humano. Nenhum dos dez resultados passou por revisão por pares formal. O precedente pesa: em outubro de 2025 o anúncio de dez problemas de Erdős «resolvidos» pelo GPT-5 revelou-se infundado, e Thomas Bloom, responsável pelo erdosproblems.com, chamou-lhe uma grave deturpação. Sobre os dez resultados de hoje, o mesmo Bloom fala antes de «big news». Como observa o físico teórico Tobias J. Osborne, os 2000 dólares citados são o custo dos tokens vencedores, não a colheita total das tentativas — um dado sobre o qual a OpenAI nada disse. Tudo isto se inscreve no contexto da «Leiden Declaration on Artificial Intelligence and Mathematics», publicada em junho de 2026 e apoiada, segundo the-decoder, por mais de 3000 matemáticos e pela International Mathematical Union, que exige transparência, proteção dos direitos dos autores e responsabilidade humana sobre os resultados.

A verdadeira notícia não é que uma máquina tenha feito matemática — acontece há meses — mas que desta vez cada resultado chega com um certificado Lean recompilável: para julgar não é preciso confiar em quem anuncia. Ainda assim, enquanto a relação entre tentativas falhadas e sucessos continuar a ser segredo industrial, avaliar a eficiência destes modelos permanecerá um exercício de fé mais do que de estatística.