A OpenAI colocou no ar, em outubro de 2026, um catálogo com 372 famílias de resultados matemáticos produzidos por um modelo interno ainda não liberado ao público. O número impressiona à primeira vista, mas ele ganha outro contorno quando se olha a estrutura por trás: são 722 manuscritos organizados em 372 famílias, ou seja, cerca de dois documentos por família, agrupando resultado principal, argumentos companheiros, consequências ou provas alternativas. A unidade real da publicação não é a prova isolada, é o agrupamento. Esse detalhe muda a leitura do número que virou manchete.
O anúncio oficial veio na página Sharing AI progress in mathematics (abre em nova aba), e o conteúdo está no repositório openai/math no GitHub (abre em nova aba), com protocolos para revisão e citação dos artigos. Para uma comunidade científica acostumada a esperar meses pelo ciclo de revisão por pares, a escolha de publicar direto em um repositório de código, com logs de revisão, é em si uma declaração de postura.
Como os resultados foram produzidos
Segundo a documentação do repositório, a grande maioria dos resultados seguiu o mesmo procedimento com o modelo interno não lançado. O modelo recebeu, ao longo da avaliação, aproximadamente 4.000 problemas. Desse total, a triagem que exigiu um "nível apropriado de significância" reduziu a saída para as 372 famílias publicadas. Cada resultado consumiu, em média, o equivalente a cerca de três horas de raciocínio no ChatGPT Pro, a assinatura premium da plataforma. A cobertura do The Decoder (abre em nova aba) acrescenta que quase todo resultado teria vindo de um único prompt a um único agente de IA, embora alguns exigiram múltiplas tentativas.
Há duas leituras possíveis para esses números de esforço computacional. A primeira é otimista: três horas de raciocínio premium por resultado sério, com uma taxa de aproveitamento de quase 10% sobre 4.000 problemas tentados, seria uma produtividade sem precedente em qualquer escala humana de pesquisa. A segunda é mais fria: o custo por resultado ainda é alto o suficiente para que a produção em massa dependa de infraestrutura proprietária e orçamento de数据中心 corporativo, e a taxa de descarte de 90% sugere que o processo é, essencialmente, busca exaustiva com filtragem, não compreensão direcionada. As evidências publicadas não permitem decidir entre as duas leituras, e a OpenAI não apresentou uma metodologia que as separe.
O catálogo abrange disciplinas variadas, e a própria empresa publicou dez resumos do raciocínio do modelo, incluindo famílias sobre correlações de dois pontos de funções multiplicativas, o expoente de irracionalidade de π e as conjecturas de Mahler simétricas e gerais. Segundo o The Decoder, a coleção inclui melhorias em algoritmos importantes e avanços relacionados à hipótese de Riemann.
O papel do Lean: verificação mecânica, não entendimento
A parte tecnicamente mais relevante para desenvolvedores é a infraestrutura de verificação. A OpenAI compartilhou formalizações de muitas das provas em Lean (abre em nova aba), uma linguagem de programação e assistente de provas em que demonstrações matemáticas podem ser checadas por computador. Em Lean, uma prova não é um texto persuasivo, é um programa cuja correção o verificador aceita ou rejeita. Se a formalização está correta, a validade do argumento é garantida pelo verificador, independentemente de quem escreveu o argumento, humano ou modelo.
Isso resolve metade do problema. O que o Lean atesta é que a cadeia de deduções é válida, não que o resultado é interessante, novo ou bem motivado. A verificação formal cobre correção lógica; a avaliação científica de significância continua dependendo de especialistas humanos. A OpenAI reconhece implicitamente essa divisão ao dizer que pretende atualizar o repositório com mais formalizações conforme as obtém, o que indica que parte do catálogo ainda está sem checagem mecânica completa. A extensão exata da cobertura formal não foi especificada com precisão nos materiais publicados.
O contra-movimento: 25 medalhistas Fields
A publicação não aconteceu no vácuo. Menos de um mês antes, em setembro de 2026, surgiu a carta aberta "A Severe Misalignment of AI in Mathematics" (abre em nova aba), assinada por 25 ganhadores da Medalha Fields, o prêmio mais alto da matemática. Os signatários incluem Terence Tao (2006), Peter Scholze (2018), Pierre Deligne (1978), Manjul Bhargava (2014), Cédric Villani (2010), Maryna Viazovska (2022), James Maynard (2022), Hugo Duminil-Copin (2022), June Huh (2022), Alessio Figalli (2018), Caucher Birkar (2018), Artur Avila (2014), Martin Hairer (2014), Maxim Kontsevich (1998), Pierre-Louis Lions (1994), Simon Donaldson (1986), Shigefumi Mori (1990), Andrei Okounkov (2006), Ngô Bảo Châu (2010), Elon Lindenstrauss (2010), Stanislav Smirnov (2010), Curt McMullen (1998), Wendelin Werner (2006), Efim Zelmanov (1994) e Yu Deng (2026).
O argumento central da carta é que a capacidade dos modelos de linguagem de resolver problemas abertos, embora real, é tratada pelas empresas de IA como benchmark, e isso seria nocivo à ciência. Na formulação dos assinantes, resolver problemas é apenas ferramenta e proxy para o objetivo real, que seria o entendimento conceitual e a percepção. A produção em massa de enunciados verdadeiros, argumentam, poderia destruir terreno fértil em vez de dar vida a novas ideias.
A carta fecha o que a Scientific American (abre em nova aba) descreveu como talvez a semana mais consequente da história da matemática: dias antes, a OpenAI havia anunciado uma solução para as equações de Navier-Stokes, um dos sete Problemas do Prêmio do Milênio. A proximidade entre o anúncio de um problema do milênio e o protesto de um quarto dos medalhistas Fields vivos não é coincidência temporal, é a própria substância do conflito.
O que está realmente em disputa
Dois modelos de valor científico colidem. Um deles mede progresso por problemas resolvidos: mais verdades provadas, mais formalizações verificadas, mais cobertura do espaço de enunciados. O outro mede progresso por compreensão: menos teoremas, mas com estruturas que revelam por que as coisas são assim. Ambos os modelos são legítimos em diferentes tradições da matemática, e a história da disciplina registra exemplos dos dois tipos, de resoluções técnicas célebres a reorganizações conceituais que mudaram campos inteiros.
O ponto cego do modelo de produção em massa é o solo de onde nascem os problemas. Se as conjecturas abertas são, em parte, um mapa do que a comunidade ainda não entende, prová-las de forma automática sem gerar entendimento pode esvaziar o mapa sem construir o território. O ponto cego do contrário é a escala: nenhuma coalizão humana, por mais brilhante, verifica formalmente 372 famílias de resultados em uma semana, e descartar esse rendimento por princípio também tem custo.
A OpenAI, por sua vez, diz ter consultado o grupo consultivo independente sobre Matemática e Inteligência Artificial do Institute for Advanced Study, usando seus conselhos para orientar a forma da publicação. O anúncio oficial em rede social resume a posição:
Estamos liberando uma ampla gama de novos resultados matemáticos produzidos por um modelo interno de fronteira. Consultamos o grupo consultivo independente sobre Matemática e Inteligência Artificial do Institute for Advanced Study, e usamos seus conselhos e recomendações públicas para orientar como liberamos esses resultados.
O que resta em aberto
A empresa prometeu atualizar o repositório com mais formalizações e manter os protocolos de revisão e citação, mas não anunciou cronograma para liberar o modelo que gerou os resultados, nem detalhou a metodologia de triagem dos 4.000 problemas. Para a comunidade Lean e mathlib, a chegada de centenas de formalizações novas é material de trabalho concreto: mais lemas, mais dependências, mais código a revisar. Para matemáticos, o repositório é tanto um recurso quanto um sintoma.
A questão que separa os campos não é se as provas estão corretas; o verificador cuida disso na medida em que as formalizações existem. A questão é o que a comunidade faz com um fluxo de verdades sem narrativa. A resposta a isso não está no README.