OpenAI afirma que seus modelos refutaram a hipótese do tempo exponencial e provaram a conjectura de Kakeya

A OpenAI anunciou em 26 de outubro três resultados científicos produzidos por seus modelos internos: uma refutação da hipótese do tempo exponencial (ETH), um pilar da ciência da computação teórica, uma prova em qualquer dimensão da conjectura de suavização local, que implica a de Kakeya, e uma prova de existência de teorias quânticas de campos, incluindo a cromodinâmica quântica. São afirmações, ainda não conquistas: a comunidade científica está apenas começando a examiná-las.

Três resultados, três domínios

Em ciência da computação teórica. A ETH postula, para simplificar, que o problema 3-SAT (decidir se uma fórmula lógica pode ser satisfeita) não pode ser resolvido em tempo subexponencial. Ela é amplamente aceita e serve de ponto de partida para centenas de artigos, que dela deduzem que um problema é difícil. A pré-publicação da OpenAI, datada de 25 de outubro, descreve um algoritmo determinístico que conta exatamente as soluções de fórmulas de largura fixa em tempo subexponencial e espaço polinomial; o caso do 3-SAT refutaria a ETH. Segundo a OpenAI, o modelo encontrou essa prova em 16 de outubro e ela foi formalizada em Lean, um assistente de prova que verifica mecanicamente cada etapa, em 17 de outubro.

Em matemática. A conjectura de suavização local, proposta por Sogge em 1991, trata da focalização de ondas. Ela havia sido demonstrada em dimensão 2 em 2019 (Guth, Wang e Zhang), e a conjectura de Kakeya em dimensão 3 em 2025 (Wang e Zahl). Os modelos da OpenAI propõem uma prova em qualquer dimensão, baseada em uma equação auxiliar de derivadas parciais. O registro do repositório é um pouco mais cauteloso que o anúncio quanto a uma das consequências: fala das estimativas de restrição de Stein “no interior” do domínio conjecturado.

Em física. O terceiro resultado é uma prova matematicamente rigorosa da existência de certas teorias quânticas de campos em quatro dimensões, incluindo a QCD, que descreve a interação forte entre quarks e glúons. Inclui a existência da teoria pura de Yang-Mills, que faz parte de um dos problemas do milênio do Instituto Clay. Nem o texto nem a formalização estão publicados: o grupo de físicos escolheu redigir ele mesmo uma apresentação.

Um novo método de publicação

A OpenAI apresenta esses manuscritos como “dados brutos de pesquisa” e pediu a especialistas de cada domínio que organizem seu exame. Para a ETH, o grupo é liderado por Russell Impagliazzo e Ramamohan Paturi, que formularam a hipótese, e por Ryan Williams (MIT). Para a física, pelo Nobel David Gross, com Michael Douglas, Arthur Jaffe, Igor Klebanov e Nikita Nekrasov. Os participantes não assinam acordo de confidencialidade, não são remunerados e falam em seu próprio nome. A OpenAI diz não reivindicar nenhum crédito acadêmico e se comprometeu, a pedido do grupo, a financiar uma conferência sobre as consequências do resultado.

Ryan Williams anunciou o exame falando de uma refutação “alegada” da ETH, e esclarece que o grupo pediu a publicação de todos os dados brutos, PDFs e código Lean incluídos.

Por que a cautela se impõe

A formalização em Lean é um argumento forte, mas só garante o que foi formalizado: ainda é preciso verificar se os enunciados verificados pela máquina correspondem aos enunciados que os pesquisadores têm em mente. O histórico da OpenAI lembra também que um erro continua possível: em 7 de outubro, a empresa retirou três manuscritos de uma publicação anterior, invalidados por um erro de sinal, e corrigiu outros quatorze.