A OpenAI divulgou em 26 de outubro, de uma só vez, três resultados de pesquisa produzidos por seus modelos de IA, nas áreas de ciência da computação teórica, análise harmônica e física matemática. O de maior peso é uma prova de que a Hipótese do Tempo Exponencial (ETH) não é verdadeira. A empresa não disse qual modelo foi usado, falando apenas em “modelos de IA da OpenAI”, e afirmou que os três resultados ainda precisam de confirmação independente da comunidade acadêmica.
ETH: a base de centenas de artigos
A Hipótese do Tempo Exponencial trata da dificuldade computacional do problema de satisfatibilidade de fórmulas booleanas (3-SAT): em linhas gerais, afirma que esse tipo de problema não pode ser resolvido em tempo subexponencial. É mais forte que “P diferente de NP” e também mais útil. Há décadas é tratada como premissa padrão, e os limites inferiores de centenas de artigos em teoria dos grafos, biologia computacional, bancos de dados e geometria computacional se apoiam nela.
Pela linha do tempo divulgada pela OpenAI, o modelo gerou a prova em linguagem natural em 16 de outubro e concluiu a formalização em Lean no dia seguinte. Participaram da colaboração Russell Impagliazzo e Ramamohan Paturi, da Universidade da Califórnia em San Diego, e Ryan Williams, do Instituto de Tecnologia de Massachusetts (MIT). Os dois primeiros estão entre os proponentes da ETH.
Segundo o que foi divulgado, os acadêmicos apresentaram duas condições à OpenAI: tornar públicos todos os dados originais e financiar uma conferência acadêmica dedicada a discutir o impacto desse resultado na ciência da computação. A OpenAI aceitou ambas. Se a prova resistir ao escrutínio, os artigos que partem da ETH terão de ser reavaliados um a um: quais conclusões apenas perdem sua condição e quais podem ser salvas com outras hipóteses é um trabalho nada pequeno.
Conjectura de Kakeya: uma linha familiar aos leitores chineses
O segundo resultado é a prova da conjectura de suavização local em todas as dimensões, da qual decorrem a conjectura de Kakeya e a conjectura de restrição de Stein em todas as dimensões. O que entra em jogo aqui é uma equação diferencial parcial auxiliar construída pelo modelo. A OpenAI afirma ter obtido a prova em 18 de outubro e concluído a formalização em Lean no dia seguinte; tanto a versão em linguagem natural quanto os arquivos Lean estão no GitHub.
Essa linha de pesquisa não é estranha aos leitores chineses. A conjectura de suavização local foi proposta por Christopher Sogge em 1991; em 2019, Larry Guth, Hong Wang e Ruixiang Zhang provaram o caso bidimensional; em 2025, Hong Wang e Joshua Zahl provaram a conjectura de Kakeya em três dimensões, vista na época como um dos avanços mais importantes da análise harmônica em muitos anos. Passar de três dimensões para todas é um salto enorme; como matemáticos externos avaliam o resultado ainda não se vê em manifestações públicas.
Yang–Mills: apenas revisão de especialistas
O terceiro resultado é de física matemática. A pesquisa demonstra, em sentido matemático rigoroso, que existem em quatro dimensões certas teorias quânticas de campos com interação que contêm ao mesmo tempo campos de gauge e férmions, incluindo a cromodinâmica quântica, e trata de passagem um subproblema da existência da teoria de Yang–Mills pura. A existência e o gap de massa da teoria de Yang–Mills pura são um dos Problemas do Milênio do Instituto Clay.
O método segue a linha da teoria quântica de campos construtiva de Tadeusz Balaban. Como o Modelo Padrão não pode ser estendido diretamente a escalas de distância arbitrariamente curtas, a prova se refere à mais simples teoria de grande unificação que contém os campos de gauge e férmions do Modelo Padrão. A revisão foi liderada pelo Nobel David Gross, com a participação de Michael Douglas, Arthur Jaffe, Igor Klebanov e Nikita Nekrasov. Este resultado não passou por verificação formal.
De maio a outubro
Se as divulgações de matemática da OpenAI neste ano forem postas em sequência, o ritmo está acelerando e o alvo está mudando. Em maio foi um problema de Erdős com oitenta anos; em setembro, o problema da suavidade das equações de Navier–Stokes, também com arquivos Lean, mas sem verificação independente concluída por matemáticos na época; desta vez trata-se de uma hipótese de complexidade computacional da qual muitos trabalhos dependem, e pela primeira vez os próprios proponentes da hipótese entram na lista de colaboradores.
A forma de verificação também se divide: os dois resultados matemáticos têm provas em Lean verificáveis por máquina, enquanto o de física só pode contar com revisão humana. O Lean garante que a dedução não tem lacunas, desde que o enunciado da proposição não tenha se desviado durante a formalização. Isso só poderá ser confirmado quando equipes independentes lerem os arquivos linha por linha.
Fontes: comunicado de pesquisa da OpenAI, CocoLoop, ITHome; arquivos de formalização em Lean publicados no GitHub, usados para conferir o objeto da prova e a forma de verificação.