OpenAI diz que seus modelos de IA refutaram uma hipótese central da ciência da computação

O que a OpenAI afirma ter provado

Em post publicado no blog da empresa em 27 de outubro de 2026, a OpenAI disse que modelos internos (sem nome ou versão divulgados) produziram manuscritos com provas em três áreas: ciência da computação, matemática e física teórica. A empresa chama os textos de "dado bruto de pesquisa", material que ainda precisa ser entendido e checado por humanos, segundo reportagem do The Decoder.

Para isso, a OpenAI recrutou grupos externos para funcionar como avaliadores de cada resultado. O tratamento varia por área: em ciência da computação e matemática, parte do material foi traduzida para Lean, uma linguagem que permite a um computador verificar, passo a passo, se uma demonstração é logicamente consistente. Em física, o grupo responsável decidiu segurar o material gerado pela IA por enquanto e escrever a prova final por conta própria.

A empresa é explícita num ponto: ela não está reivindicando o crédito científico pelas descobertas. Segundo o The Decoder, isso parece resposta às críticas recebidas depois do episódio conhecido como "desastre de relações públicas do Navier-Stokes", quando um anúncio anterior da OpenAI sobre resultados matemáticos foi recebido com desconfiança pela comunidade acadêmica.

A hipótese que sustenta boa parte da teoria da complexidade

O resultado de ciência da computação mexe com a Exponential Time Hypothesis (ETH), uma suposição sobre o problema da satisfatibilidade booleana, ou SAT. Numa instância de SAT, você tem uma fórmula lógica com variáveis que só podem ser verdadeiras ou falsas, e a pergunta é se existe uma combinação que torna a fórmula inteira verdadeira.

Com poucas variáveis dá para testar cada combinação na força bruta. O problema é que cada variável nova dobra o número de possibilidades: com 100 variáveis já se chega a um número de 31 dígitos. A ETH diz que não existe atalho real para isso: você pode otimizar a busca, mas no pior caso o tempo de computação continua crescendo de forma exponencial a cada variável adicionada.

SAT é considerado o problema canônico dessa família difícil, e está diretamente ligado ao P versus NP, a questão em aberto mais famosa da computação (se todo problema cuja solução é fácil de checar também é fácil de resolver). A ETH vai além do P diferente de NP: ela não diz só que SAT é difícil, diz exatamente o quão difícil. Centenas de artigos em teoria dos grafos, biologia computacional, bancos de dados e geometria computacional usam a ETH como alicerce para provar limites de velocidade de outros algoritmos.

A OpenAI afirma que seu sistema provou que a ETH é falsa. Se a prova se confirmar, esses artigos perdem a base formal em que se apoiavam: os resultados não ficam automaticamente errados, mas deixam de estar provados.

O que muda, e o que não muda, pra quem usa SAT solvers

Aqui entra o recorte que interessa a quem constrói software de verdade. Programas chamados SAT solvers são usados hoje para checar erros em projetos de chips e para testar software, entre outras aplicações, e já lidam rotineiramente com fórmulas de milhões de variáveis. Isso é possível porque os casos do mundo real costumam ser muito mais fáceis do que o pior caso teórico que a ETH descreve. Acelerar só o pior caso não ajuda automaticamente essas ferramentas.

O professor do MIT Ryan Williams, que vai ajudar a verificar o resultado de forma independente, foi perguntado no X o que desenvolvedores comuns notariam primeiro. Sua resposta foi direta:

Ou podemos não ver nada disso. Eu realmente não sei.

Or we may see nothing of the sort. I really don't know.Ryan Williams, professor do MIT

Williams disse que, no ritmo atual, é plausível que avanços práticos em resolução de SAT apareçam dentro de 12 meses, mas também admitiu que pode não acontecer nada disso. O impacto imediato do resultado, segundo ele, é mais teórico: se a prova se sustentar, uma classe de problemas muito exigentes não poderia ser resolvida com circuitos pequenos (circuitos em que, dobrando o tamanho da entrada, o número de portas lógicas no máximo dobra também).

Lean confirma lógica, não confirma o problema certo

Vale entender o que a tradução para Lean garante e o que ela não garante, porque é um ponto que confunde até quem já ouviu falar de verificação formal. Lean checa se uma demonstração estabelece, de fato, o enunciado tal como foi escrito na própria linguagem Lean. Isso não garante que esse enunciado captura corretamente o problema que os matemáticos queriam resolver: essa tradução de linguagem natural para formalismo ainda depende de julgamento humano.

Por isso, a checagem automática não substitui a revisão por pares. No caso da ETH, o grupo que a propôs originalmente, formado por Russell Impagliazzo e Ramamohan Paturi (da UC San Diego) ao lado de Francis Zane, é quem está revisando agora se a hipótese está errada, junto com Williams, que não integrou a formulação original mas participa da checagem atual. Eles afirmam, em carta aberta, não ter assinado acordo de confidencialidade, estar trabalhando sem remuneração e pretender compartilhar achados parciais conforme avançam. Também deixam claro que participar da checagem não é um aval ao resultado.

A pedido desse grupo, a OpenAI publicou todos os dados brutos, incluindo o texto da prova e o arquivo Lean correspondente, e se comprometeu a financiar uma conferência sobre o significado do resultado para a área.

Uma conjectura de ondas de 1991 resolvida em todas as dimensões

O resultado de matemática envolve a conjectura de suavização local (local smoothing conjecture), proposta pelo matemático Christopher Sogge em 1991. Ela descreve como ondas, sejam sonoras, luminosas ou sísmicas, podem se concentrar intensamente num único ponto por um instante, como a luz no foco de uma lupa, mas em média se comportam de forma mais suave do que esse pico sugeriria.

Até agora a conjectura só tinha sido provada em duas dimensões, para ondas numa superfície como a água, trabalho feito por Guth, Wang e Zhang em 2019. A OpenAI diz que seus modelos produziram uma prova válida para qualquer número de dimensões, incluindo o espaço tridimensional comum e espaços hipotéticos com mais dimensões.

O motivo de isso importar além da física das ondas é que duas outras conjecturas famosas decorrem diretamente dela: a conjectura de Kakeya, da geometria, e a conjectura de restrição de Stein, da análise de Fourier (a técnica que decompõe sinais, como sons, em oscilações individuais). A conjectura de Kakeya só tinha sido provada em três dimensões, por Wang e Zahl em 2025. Se o resultado da OpenAI se confirmar, as duas ficariam provadas em todas as dimensões de uma vez.

Diferente dos outros dois casos, esse resultado não tem um grupo dedicado de verificação. A OpenAI diz ter consultado um especialista externo sobre como estruturar essa checagem e, por recomendação dele, optou por publicar diretamente o texto da prova e o arquivo Lean, deixando a comunidade matemática livre para decidir como validar.

O problema do milênio que continua sem solução completa

O resultado de física mira a base matemática da teoria quântica de campos, o arcabouço usado para descrever partículas elementares e as forças entre elas. As previsões dessa teoria são extremamente precisas, mas faltava uma base matemática rigorosa: os físicos trabalham com aproximações, como uma rede imaginária de pontos que vai sendo refinada, sem saber ao certo se isso converge para uma teoria única e consistente.

A OpenAI afirma ter provado que certas teorias quânticas de campos existem matematicamente em quatro dimensões (três de espaço mais o tempo), algo que ninguém havia conseguido para teorias em que as partículas interagem entre si. O caminho passa por três teorias encadeadas: a teoria de Yang-Mills, que descreve só os glúons (as partículas que carregam a força forte, responsável por unir quarks em prótons e nêutrons); a cromodinâmica quântica, que adiciona os quarks; e a mais simples teoria de grande unificação, que reúne três das quatro forças fundamentais.

A teoria de Yang-Mills é, especificamente, um dos sete Problemas do Milênio do Clay Mathematics Institute, cada um com prêmio de 1 milhão de dólares. O problema tem duas partes: provar que a teoria existe matematicamente, e provar que ela tem o chamado "gap de massa" (a explicação matemática de por que a força forte, carregada por partículas sem massa na equação, só age a distâncias minúsculas, diferente do eletromagnetismo). A OpenAI é explícita: resolveu só a parte da existência. O Problema do Milênio continua, portanto, sem solução completa, e sem o prêmio de 1 milhão de dólares reivindicado.

Quem está revisando esse resultado é um grupo liderado por David Gross, que dividiu o Nobel de Física de 2004 por trabalho sobre liberdade assintótica (o fenômeno que, segundo a OpenAI, é justamente o que torna essas teorias matematicamente administráveis). O grupo inclui também Arthur Jaffe, um dos autores do enunciado oficial do Problema do Milênio de Yang-Mills.

O que ainda está em aberto

A própria OpenAI reconhece trade-offs no processo: quem escolhe os primeiros revisores influencia quem tem acesso à informação antes de todo mundo, e a empresa diz não saber ainda qual dos três modelos de checagem (tradução para Lean com grupo dedicado, publicação direta dos dados, ou retenção do material até um grupo escrever a versão final) funciona melhor.

A empresa também anunciou doação de 5 milhões de dólares à Simons Foundation para financiar workshops e conferências sobre resultados de IA em pesquisa. O grupo de Williams, por sua vez, usa a carta aberta para pedir um debate mais amplo que vá além da checagem técnica: como verificar descobertas feitas por IA, quem tem acesso a elas primeiro e a quem cabe o crédito quando a demonstração final sai de um modelo e não de um pesquisador.

Para quem decide onde a IA entra num fluxo de engenharia, o episódio é um lembrete prático: resultado de modelo de linguagem em matemática pesada não é, por enquanto, algo para aceitar sem checagem formal e revisão humana, mesmo quando vem acompanhado de arquivo Lean. A prova formal garante consistência lógica interna, não garante que o problema resolvido é o problema que interessa.

Fonte: The Decoder