Como avaliar os 722 manuscritos matemáticos da OpenAI

Se você leu que a OpenAI resolveu centenas de problemas abertos, a fonte primária diz outra coisa. Dos 722 manuscritos matemáticos da OpenAI, cerca de 560 não têm o resultado principal formalizado, e o próprio README admite que resultados sem verificação podem conter erros.

O que a OpenAI publicou em 6 de outubro de 2026

A OpenAI publicou 722 manuscritos matemáticos em 372 famílias de resultados no dia 6 de outubro de 2026, por volta das 18h no horário do Leste dos Estados Unidos. Segundo o README do próprio repositório, o modelo recebeu cerca de 4.000 problemas, e cada resultado consumiu em média 3 horas de computação de raciocínio.

Alguns números pedem cuidado. As 4.000 tentativas não formam uma taxa de sucesso, porque o material não informa quantos problemas não geraram manuscrito algum. A imprensa também contou de formas diferentes: a Scientific American citou 372 resultados, enquanto o repositório fala em 722 manuscritos agrupados em 372 famílias, em que uma família reúne artigos relacionados.

Um porta-voz afirmou que o modelo produziu quase todos os resultados a partir de um único prompt dado a um único agente de IA. Essa é a versão da empresa sobre o processo. Fora dela, ninguém consegue reproduzir o experimento, porque a OpenAI não divulgou o nome do modelo nem os prompts. Andrew Sutherland, matemático do MIT, disse que essas alegações devem ser tratadas como não verificadas até que o modelo seja liberado.

Quantos resultados o Lean realmente verificou

Aproximadamente 162 dos 722 manuscritos têm o resultado principal confirmado por uma formalização no Lean, segundo contagem divulgada por veículos de imprensa. Isso fica pouco abaixo de um quarto do total, e cerca de 560 manuscritos seguem sem prova formal completa do resultado principal.

A fonte mais conservadora aqui é a própria OpenAI. O README do lançamento diz que nem todos os resultados têm formalização no Lean e que "alguns dos resultados não formalizados podem ter problemas". É um aviso escrito pela empresa, não por críticos. Até 7 de outubro de 2026, não existia revisão por pares independente nem replicação, então ninguém sabe quantos manuscritos estão corretos.

Para facilitar a leitura, o arquivo CONTENTS do repositório lista os resultados de destaque com o status de verificação. A tabela abaixo resume os exemplos mais citados:

Resultado	Status no arquivo da OpenAI
Irracionalidade da constante de Catalã	Marcado como verificado no Lean
Conjectura de Chowla para dois pontos	Marcado como verificado no Lean
Contraprova à cancelamento de Zariski em dimensão 4	Marcado como verificado no Lean
Zero-free line para funções L de Hecke sobre Q(√-3)	Marcado como verificado no Lean
Hilbert 10 sobre os racionais	Sem verificação Lean listada
Fórmula ligada à conjetura de Birch e Swinnerton-Dyer	Sem verificação Lean listada

As fontes divergem em alguns itens, e os números são aproximados porque cada relatório conta em unidades diferentes. Se um resultado aparece sem marca de verificação, trate-o como afirmação, não como teorema.

O que o Lean garante e o que ele não checa

O Lean é um verificador de provas que aceita ou rejeita cada passo lógico de uma demonstração escrita em linguagem formal. Alguém, humano ou modelo, digita a prova, e o sistema testa cada inferência. Se um passo falha, a prova inteira é rejeitada, sem depender da confiança no autor.

Essa garantia tem três limites claros, e vale listá-los na ordem em que aparecem no debate:

1. O Lean confere se os passos são válidos, e só isso.
2. Ele não confere se o enunciado digitado corresponde ao problema aberto de fato. Um enunciado mais fraco pode passar com uma prova correta de outra pergunta.
3. Ele não produz compreensão. Uma prova pode passar no verificador enquanto nenhum humano consegue explicá-la.

Terence Tao, medalhista Fields e professor da UCLA, falou em "indigestão de provas" em um evento no Caltech em 11 de setembro de 2026: o Lean aprova a prova, mas humanos ainda precisam lê-la e entendê-la. Em janeiro de 2025, o mesmo Tao havia defendido a verificação formal, escrevendo que na matemática é possível checar completamente as saídas e filtrar boa parte do lixo. As duas posições se encaixam: o filtro confere correção, não entendimento.

A implicação prática é simples. Um "passou no Lean" responde só a primeira de três perguntas, e as outras duas continuam com pessoas.

"Quase-Hipótese de Riemann" não é a Hipótese de Riemann

O artigo de destaque do lançamento não prova a Hipótese de Riemann. O que o manuscrito estabelece é uma faixa sem zeros para funções L de Hecke sobre um único corpo de números, o conjunto dos racionais estendido pela raiz quadrada de menos três, onde a parte real de s fica acima de 7/8.

A distinção importa. A Hipótese de Riemann trata dos zeros da função zeta de Riemann e exigiria empurrar essa fronteira de 7/8 até a reta crítica de 1/2, cobrindo a própria função zeta. O artigo cobre funções relacionadas, mas não a zeta, e o arquivo da OpenAI marca o resultado como checado no Lean sem confirmação independente registrada.

Se você vir a manchete "OpenAI prova Riemann", ela está errada. O nome do artigo, com o prefixo "quasi", já sinaliza que o enunciado é mais fraco do que o problema famoso que ele evoca.

Sigilo, crédito e a revolta dos matemáticos

O conflito central não é sobre uma prova específica, e sim sobre como o trabalho foi lançado. A Quanta Magazine noticiou em 5 de outubro de 2026, um dia antes da publicação, que a OpenAI mantinha mais de 100 resultados em sigilo. As fontes não dizem quantos deles estão entre os 722.

Existem dois eixos de disputa:

• Reproduzibilidade. Um grupo consultivo independente sobre matemática e IA, hospedado no Institute for Advanced Study desde setembro de 2026 e com membros como Gowers e Witten, recomendou que a OpenAI divulgasse nomes de modelos, prompts e computação, além de depositar os artigos em repositórios acadêmicos. O lançamento trouxe apenas um tempo médio de computação e 10 resumos de raciocínio, deixando de fora o modelo e os prompts.

• Crédito e ritmo. Relatos secundários dizem que matemáticos saíram de uma reunião em agosto com a impressão de que a empresa não soltaria tudo de uma vez. Também se atribui a dois humanos, Diego Córdoba e Luis Martínez Zoroa, o insight-chave de uma reivindicação anterior sobre Navier-Stokes, informação vinda de fonte única e não confirmada. Tao resumiu o clima pedindo desaceleração: "temos que desacelerar, o ritmo é insano".

A consequência organizacional aparece na Quanta Magazine: matemáticos passaram a publicar preprints antes da revisão para registrar a data da descoberta antes que um modelo os supere, enquanto a atividade no MathOverflow cai e o arXiv discute limites de submissão. Um pesquisador entrevistado disse que o sistema foi levado ao limite e quebrado. Se modelos escrevem mais rápido do que humanos leem, a fila cresce todo dia.

A lição para quem constrói com agentes de IA

O caso dos manuscritos matemáticos da OpenAI ilustra um padrão útil fora da matemática: a confiança no output de um agente depende da força do verificador. A matemática tem o Lean, que rejeita provas erradas passo a passo; a maioria do trabalho de software tem suítes de testes, que podem deixar passar um problema exatamente como o Lean certifica o enunciado errado.

Há também um limite de monitoramento. Um artigo assinado por 42 pesquisadores de vários laboratórios argumenta que monitorar cadeias de raciocínio pode revelar intenção de má conduta, mas chama esse monitoramento de promissor, imperfeito e frágil. No lançamento, terceiros viram pouco: 10 resumos curtos para 722 manuscritos, sem o raciocínio completo.

O veredito honesto tem três partes. Uma contagem aponta verificação computacional para só uma minoria dos manuscritos. A OpenAI não liberou modelo nem prompts. E os matemáticos que devem julgar os resultados estão publicando cedo e discordando em público. A matemática não morreu; o que falhou é a suposição de que humanos conseguem ler tudo o que máquinas produzem.

Perguntas frequentes

• A OpenAI provou a Hipótese de Riemann? Não. O artigo marca uma faixa sem zeros para funções L de Hecke sobre Q(√-3) acima da parte real 7/8. Ele não cobre a função zeta de Riemann nem atinge a reta crítica de 1/2.

• Quantos dos manuscritos matemáticos da OpenAI estão verificados? Cerca de 162 dos 722 têm o resultado principal formalizado no Lean, segundo contagem divulgada por veículos de imprensa. O próprio README da OpenAI admite que resultados sem formalização podem ter problemas.

• Um resultado marcado como "Lean checked" está correto? Significa que a OpenAI declara que o Lean aceitou a prova do enunciado digitado. O verificador não garante que o enunciado equivale ao problema aberto nem que humanos entendem a prova, e não havia confirmação independente até 7 de outubro de 2026.

• Por que os matemáticos estão publicando preprints tão cedo? Porque um preprint registra a data da reivindicação. Se uma empresa pode manter mais de 100 resultados em segredo, o pesquisador não sabe se um problema já foi resolvido, e publicar cedo protege o crédito.

• Posso reproduzir os resultados da OpenAI? Não por enquanto. A empresa não divulgou o nome do modelo, os prompts nem o raciocínio completo, e o grupo consultivo independente recomendou exatamente essas divulgações.

Source video