OpenAI diz ter provado Yang-Mills e refutado ETH. Revisores avisam: isso não é validação

Em 26 de outubro, a OpenAI publicou um anúncio reunindo três resultados gerados por modelos internos da empresa. O primeiro: um dos modelos encontrou, em 16 de outubro, uma refutação da Exponential Time Hypothesis (ETH), conjectura fundamental em ciência da computação usada em centenas de papers. A prova foi formalizada no sistema Lean no dia seguinte.

No mesmo anúncio, a empresa alega ter provado a conjectura de alisamento local (o que resolveria as conjecturas de Kakeya e restrição de Stein) e a existência da teoria de Yang-Mills pura em quatro dimensões — um resultado parcial do Problema do Milênio do Clay Mathematics Institute sobre Yang-Mills, que também exige provar a existência de um "mass gap" (lacuna de massa). A OpenAI não alega ter resolvido essa segunda parte.

Há um detalhe que separa esse anúncio de um resultado científico consolidado: os próprios revisores escolhidos pela OpenAI já sinalizaram que nenhuma validação está acontecendo.

O que a OpenAI diz ter provado

A OpenAI apresentou três alegações principais com o seguinte cronograma:

• 16/10/2026: o modelo encontra a refutação da Exponential Time Hypothesis.
• 17/10/2026: a prova é verificada em Lean, linguagem de demonstração assistida por computador.
• 18/10/2026: o modelo gera a prova da conjectura do alisamento local, que resolve Kakeya e restrição de Stein.
• 19/10/2026: essa prova também é formalizada em Lean.

A alegação sobre Yang-Mills seguiu um cronograma próprio e teve sua formalização em Lean concluída também em 16 de outubro. A OpenAI consolidou as três alegações no anúncio de 26 de outubro.

A OpenAI não revelou qual modelo interno produziu as provas, nem especificou se é uma versão de pesquisa ainda não lançada. O material da refutação da ETH e da prova de alisamento local foi publicado no GitHub para escrutínio externo. O material da prova de Yang-Mills não foi liberado — o motivo está na seção abaixo.

Quem está revisando e o que eles já disseram

Para a refutação da ETH, a OpenAI acionou dois dos autores originais da hipótese: Russell Impagliazzo e Ramamohan Paturi, ambos da UC San Diego, além de Ryan Williams, do MIT. Em carta aberta, o trio foi direto: "Nossa participação não deve ser entendida como certificação da alegação. Um resultado dessa significância requer escrutínio cuidadoso e independente."

Para a prova de Yang-Mills, o grupo revisor é liderado pelo Nobel de Física David Gross, com Michael Douglas, Arthur Jaffe, Igor Klebanov e Nikita Nekrasov. Segundo a Interesting Engineering, esse grupo decidiu nem liberar ainda o material gerado pelo modelo — primeiro querem desenvolver sua própria explicação do resultado antes de divulgar qualquer coisa.

Ou seja: nos dois casos mais sensíveis, cientistas de prestígio aceitaram olhar o material, mas nenhum deles assinou embaixo.

Por que a ressalva importa

Formalização em Lean garante que uma cadeia de deduções lógicas está correta dentro do sistema formal usado. Não garante, por si só, que a prova resolve o problema do jeito que se afirma, nem substitui a leitura humana que detecta se as premissas foram definidas corretamente ou se há um salto conceitual escondido atrás da formalização.

É exatamente esse espaço que os revisores sinalizaram. A prova pode estar certa. Também pode conter uma falha sutil que só aparece depois de meses de escrutínio — como aconteceu antes: provas aparentemente fechadas fracassaram na revisão por pares.

A comunidade de ciência da computação reagiu com desconfiança. No Hacker News, a publicação sobre o caso teve mais de 400 pontos, com comentários que questionam a validade do resultado antes de qualquer verificação independente — reação típica quando uma empresa com interesse comercial direto no resultado é também quem anuncia o resultado.

O que isso significa para quem acompanha IA de ponta

O episódio é um caso de manual sobre como separar anúncio corporativo de ciência confirmada. A OpenAI tem interesse evidente em mostrar que seus modelos superam matemáticos e físicos humanos em tarefas de prova formal — é a narrativa que sustenta parte da avaliação da empresa e do argumento de que a IA está perto de acelerar a pesquisa científica.

Isso não torna as provas falsas. Torna a verificação independente a única coisa que decide se elas são reais.

O que acompanhar

Três sinais vão indicar se o anúncio se sustenta:

• Publicação formal do parecer de Impagliazzo, Paturi e Williams sobre a ETH — ainda sem data definida.
• Liberação do material de Yang-Mills pelo grupo de David Gross, hoje retido até que eles produzam sua própria explicação do resultado.
• Submissão de qualquer um dos três resultados a revista revisada por pares ou a uma conferência da área, o que ainda não ocorreu.

Até que isso aconteça, o correto é tratar os três anúncios como alegações da OpenAI, não como teoremas estabelecidos — e, no caso de Yang-Mills, como uma prova de existência, não a resolução completa do Problema do Milênio.