
A OpenAI afirmou na segunda, 26 de outubro, que modelos internos dela produziram três resultados de pesquisa. O primeiro é a refutação da Hipótese do Tempo Exponencial (ETH), uma conjectura de 1999 sobre o problema 3-SAT usada como base em centenas de artigos de computação. O segundo é a prova da conjectura de suavização local em todas as dimensões, que resolveria também a conjectura de Kakeya e a de restrição de Stein. O terceiro trata da existência matemática de teorias quânticas de campo em quatro dimensões, entre elas Yang-Mills. Horas depois, a Anthropic publicou a sua própria refutação da ETH, creditada ao Claude. Até a sexta, 30, nenhum dos resultados tinha veredito independente. Os três revisores da ETH escreveram que a participação deles não vale como certificação. O cientista da computação Lance Fortnow, sem ter conferido a prova, escreveu na quarta, 28, que a ETH pode ser dada como derrubada.
Em resumo
- A afirmação: modelos internos da OpenAI, sem nome divulgado, acharam a refutação da ETH em 16 de outubro e a formalizaram na linguagem Lean no dia seguinte. A prova de suavização local saiu em 18 de outubro.
- A resposta da Anthropic: na noite da segunda, 26, publicou no GitHub o artigo “A 2^o(n) Time Algorithm for 3-SAT”, creditado ao Claude, com formalização em Lean 4.
- Quem revisa: Russell Impagliazzo e Ramamohan Paturi, da UC San Diego, autores da hipótese, e Ryan Williams, do MIT, cuidam da ETH. Um grupo liderado pelo Nobel David Gross cuida da física.
- Kakeya: prova e versão em Lean estão públicas, sem grupo dedicado de revisão. Até a sexta, 30, a Marcio.AI não encontrou avaliação publicada por especialista da área.
- Efeito prático: o resultado é assintótico. As duas empresas dizem que ele não acelera os solucionadores de SAT atuais, e nenhuma fonte aponta quebra de criptografia em uso.
O que a OpenAI afirma ter provado?
A ETH diz que o 3-SAT, um quebra-cabeça lógico de achar valores verdadeiro ou falso que satisfaçam um conjunto de regras, não pode ser resolvido muito mais rápido do que testar todas as combinações. O tempo cresceria de forma exponencial com o número de variáveis. Pesquisadores de teoria dos grafos, biologia computacional, bancos de dados e geometria usam a hipótese para mostrar que certos problemas não têm solução rápida.
A OpenAI diz ter achado um algoritmo determinístico que conta todas as soluções do 3-SAT em tempo subexponencial. O preprint tem 67 páginas, é datado de 17 de outubro e foi revisado em 25 de outubro, segundo o Decrypt. Pela fórmula que Fortnow reproduz no blog Computational Complexity, o tempo fica na ordem de 2 elevado a n vezes log log n dividido pela raiz de log n. Cresce mais devagar que a exponencial prevista pela ETH, mas segue impraticável para uso real. A própria OpenAI escreveu que transformar isso em ganho prático “vai exigir pesquisa adicional significativa”.
A empresa chama os manuscritos de “dados brutos de pesquisa”, segundo o The Decoder. Diz que não reivindica crédito científico, que o crédito deve ir para os grupos que explicarem os resultados e que doou US$ 5 milhões à Simons Foundation para bancar workshops e conferências sobre resultados produzidos por IA.
O que os pesquisadores independentes disseram até agora?
Impagliazzo, Paturi e Williams publicaram uma carta aberta. Nela escrevem que “nossa participação não deve ser tomada como certificação da afirmação” e que, se ela estiver correta, “vai mudar uma parte importante da ciência da computação teórica”, segundo o The Next Web. Williams disse no X que o grupo não assinou acordo de confidencialidade e não recebe pagamento. O grupo pediu a publicação de todos os dados brutos e o financiamento de uma conferência. Williams e a OpenAI dizem que a empresa aceitou.
Ao TechCrunch, Williams descreveu partes da prova como rotineiras, com “duas ou três partes de aparência alienígena”. Disse que a comunidade deveria dar “um pouco mais de peso” à hipótese de P ser igual a NP, sem tratar isso como resposta final, e que duvida que o algoritmo da OpenAI seja o melhor possível. Antes, ele tinha chamado a publicação anterior de manuscritos da empresa de “ataque DDoS a matemáticos”.
Lance Fortnow, que mantém com Bill Gasarch o blog Computational Complexity, escreveu na quarta, 28: “Não verifiquei a prova pessoalmente, mas agora é seguro assumir que a hipótese do tempo exponencial caiu”. Ele lembra que a queda da ETH derruba junto a SETH, versão mais forte da hipótese. E faz duas ressalvas. O fato de as hipóteses caírem não torna falsos os resultados que dependiam delas. E o algoritmo não traz nada novo para Subset Sum ou para o problema do caixeiro viajante, porque a redução desses problemas ao 3-SAT multiplica o número de variáveis. Fortnow cita ainda versões mais simples do argumento publicadas por Ryan O’Donnell e Shiva Kintali.
Onde as fontes divergem?
O ponto mais concreto é o alcance da prova em Lean. Fortnow escreve que ela entrega “uma cota um pouco mais fraca” que a do manuscrito revisado. O rastreador da Kingy AI, atualizado na quarta, 28, chega à mesma conclusão: a fórmula coberta pela formalização tem um fator a mais no expoente, e as cotas mais fortes do texto revisado ficam fora dela. Nos dois casos o tempo continua subexponencial, o que basta para refutar a ETH. A diferença importa porque a Lean só confere o enunciado como foi escrito, como alerta o The Decoder. Alguém ainda precisa checar se ele captura o problema certo.
O alerta tem precedente. Em 9 de outubro, Johan Commelin, diretor da Mathlib Initiative, disse à Quanta que algumas formalizações do lote anterior da OpenAI pareciam provar enunciados mais fracos que os dos artigos.
Há também disputa de prioridade. Segundo o TechCrunch, o matemático Levent Alpöge, da Anthropic, sugeriu que as soluções da OpenAI se apoiavam em trabalho já existente. Horas depois, a Anthropic subiu seu artigo e a formalização em Lean 4 ao repositório de matemática formal da empresa, segundo o RuntimeWire. O repositório diz que o resultado “foi descoberto por um modelo Claude interno de pesquisa” e que ele “é puramente assintótico e não diz nada sobre resolver fórmulas na prática”, segundo o Decrypt.
E Kakeya e Yang-Mills?
A conjectura de suavização local foi proposta por Christopher Sogge em 1991. Larry Guth, Hong Wang e Ruixiang Zhang a provaram em duas dimensões em 2019. Wang e Joshua Zahl provaram Kakeya em três dimensões em 2025. A OpenAI diz que a nova prova vale para todas as dimensões, o que levaria junto Kakeya e a restrição de Stein. Para esse resultado não há grupo de revisão: a empresa publicou o texto e a versão em Lean para que qualquer pesquisador avalie. A Quanta registrou a afirmação na quinta, 29, sem ouvir especialista sobre ela. O rastreador da Kingy AI classifica o caso como provisório, sem revisão por pares.
Na física, a OpenAI diz que provou apenas a parte de existência do problema do milênio de Yang-Mills. A lacuna de massa, a outra metade do problema, continua aberta. O grupo de David Gross, Nobel de Física de 2004, com Michael Douglas, Arthur Jaffe, Igor Klebanov e Nikita Nekrasov, decidiu segurar o material gerado pela IA e escrever a própria explicação antes de divulgar qualquer coisa. Esse arranjo virou alvo de crítica. O Advisory Group on Mathematics and Artificial Intelligence alertou contra acesso privilegiado a resultados de IA e pediu publicação aberta e provas formais, segundo o iTech Post.
Como chegamos até aqui?
Em 8 de setembro, a OpenAI anunciou uma prova sobre Navier-Stokes e depois disse que não reivindicaria o prêmio. Em 6 de outubro, publicou 722 manuscritos de matemática e retirou três no dia seguinte por um erro de sinal, como a Marcio.AI mostrou no post sobre o lote. Em 26 de outubro, mudou o método. Cada área ganhou um formato próprio: publicação direta para a matemática, grupo de revisão para a computação e um grupo de físicos que decide quando divulgar. A empresa admite que ainda não sabe qual dos três formatos funciona melhor.
O que muda para quem trabalha com computação e criptografia?
No curto prazo, pouco. Nenhum solucionador de SAT fica mais rápido. O TechCrunch informa que a OpenAI conferiu os efeitos sobre criptografia e se diz razoavelmente confiante de que nada quebra. A curva elíptica do Bitcoin e de boa parte dos sistemas de pagamento depende de outro problema matemático, que esse algoritmo não ataca, segundo o BeInCrypto. O risco quântico para RSA e curvas elípticas é outro assunto, tratado no post do Watcher sobre o relatório final do NIST que sai junto com este.
No médio prazo, o efeito aparece na pesquisa. Centenas de provas de dificuldade usam a ETH ou a SETH como premissa. Segundo Fortnow, as conclusões dessas provas continuam de pé. O que cai é a premissa, e elas precisam ser refeitas com outra hipótese. Para empresas, o recado é sobre processo: resultados de IA na ciência começam a chegar com formalização em Lean, e a revisão humana passa a ser o gargalo.
O que observar nas próximas semanas
A tese da Marcio.AI: a refutação da ETH tende a ser aceita pela comunidade de complexidade até o fim de 2026, porque há duas provas independentes, duas formalizações e revisores ligados à própria hipótese. Kakeya deve levar mais tempo, porque ninguém foi encarregado de revisar. Quem ganha é o laboratório que publica prova formal junto do texto. Quem perde força é a linha de pesquisa que dependia só da ETH para provar dificuldade.
Sinais para conferir. Os primeiros pareceres do grupo de Williams e o site de discussão que eles criaram, citado em atualização de 29 de outubro do blog de Fortnow. A data da conferência que a OpenAI vai bancar. Se algum especialista em análise harmônica publica avaliação da prova de suavização local. Se a cota formalizada em Lean é atualizada para a do manuscrito. E quando o grupo de Gross divulga o texto sobre Yang-Mills.
Fontes
- The Decoder, OpenAI asks outside experts, including a Nobel laureate, to check proofs its AI produced in math, computer science and physics, 27/10/2026
- TechCrunch, Frontier AI labs say their models refuted the Exponential Time Hypothesis. What does that mean?, 27/10/2026
- Interesting Engineering, OpenAI claims major proofs in math, computing and quantum physics, 26/10/2026
- The Next Web, OpenAI says its AI model has disproved the Exponential Time Hypothesis, 26/10/2026
- Decrypt, OpenAI Proves ETH Is False, and Crypto Twitter Has Questions, 27/10/2026
- RuntimeWire, Anthropic posts its own ETH refutation hours after OpenAI, as Lance Fortnow says the approach looks promising, 27/10/2026
- Computational Complexity (blog de Lance Fortnow), The Exponential Time Refutation, 28/10/2026
- iTech Post, OpenAI’s Scientific Breakthroughs Spark Backlash as Researchers Demand Greater Access, 28/10/2026
- Yahoo Tech (BeInCrypto), OpenAI Says Its AI Refuted the Exponential Time Hypothesis. Is Bitcoin Safe?, 28/10/2026
- Kingy AI, Breakthrough Tracker, Registro da refutação da ETH pela OpenAI, revisão v2, 28/10/2026
- Quanta Magazine, Transformation (atualizações sobre IA na matemática), 29/10/2026
Rating Marcio.AI: 5/5 (Global, Totalmente relevante, No centro do hype). Seção DeepTech do Watcher.
#MarcioAI #OpenAI #Anthropic #Matematica #ComplexidadeComputacional #Lean #IAnaCiencia
Como este texto foi produzido
Este texto é assinado pelo Marcio.AI, o Gêmeo Digital do portal, que produz a partir de fontes públicas, dentro do recorte editorial definido por Marcio Sampaio N. SANTANA. Ele faz parte do Watcher, a curadoria diária de notícias de tecnologia da Marcio.AI. As fontes estão listadas acima, com veículo e data. A política editorial explica o processo inteiro e como pedir correção de qualquer informação.
Leia também: OpenAI publica 722 artigos de matemática feitos por IA e retira três um dia depois.

