A IA acabou de fazer algo que nenhum humano conseguiu em décadas

No sábado, 26 de outubro de 2026, a OpenAI publicou um post discreto no seu blog. Sem evento ao vivo, sem keynote, sem Sam Altman no palco. Apenas um texto técnico com três links para papers. O conteúdo? Três provas científicas geradas por modelos de IA que, se confirmadas, representam avanços que matemáticos, físicos e cientistas da computação perseguiam há décadas.

Eu li o anúncio duas vezes porque achei que estava entendendo errado. A primeira prova resolve uma conjectura aberta em análise harmônica. A segunda refuta uma hipótese fundamental da ciência da computação. A terceira entrega uma demonstração rigorosa de existência para teorias quânticas de campo em quatro dimensões. Tudo isso verificado formalmente em Lean, um assistente de provas que não aceita “mais ou menos certo” como resposta.

Vamos desmontar cada uma dessas provas, entender o que elas significam na prática e, mais importante, analisar por que uma parte da comunidade científica está comemorando enquanto a outra está de braços cruzados.

Prova 1: A Conjectura de Kakeya (finalmente) caiu

A conjectura de Kakeya é um desses problemas que parece simples na superfície e te engole quando você mergulha. A pergunta original, formulada em 1917 pelo matemático japonês Soichi Kakeya, era: qual é a menor área em que você consegue girar uma agulha de comprimento 1 em 360 graus?

A versão moderna do problema evoluiu para algo muito mais abstrato. Em análise harmônica, a conjectura de Kakeya afirma que certos conjuntos (chamados “Kakeya sets”) em dimensões altas têm dimensão de Hausdorff igual à dimensão do espaço. Parece críptico, mas é um resultado que conecta geometria, análise de Fourier e equações diferenciais parciais.

O que a IA da OpenAI produziu foi uma prova de “local smoothing” para ondas em toda dimensão espacial maior ou igual a dois. Essa prova, como consequência, resolve tanto a conjectura de Kakeya (nas versões maximal e dimensional) quanto as estimativas de restrição esférica de Stein.

A prova foi gerada em 18 de outubro de 2026. No dia seguinte, 19 de outubro, ela foi formalizada em Lean. Sim, um dia. Para contextualizar: em 2023, Terence Tao e outros matemáticos resolveram uma versão parcial da conjectura de Kakeya em três dimensões, e isso consumiu meses de trabalho. Agora estamos falando de todas as dimensões, resolvidas em horas.

Os matemáticos designados para avaliar o resultado incluem nomes de peso. A verificação formal em Lean é um ponto forte: o assistente de provas confere cada passo lógico, e se algo estiver errado, ele rejeita. Mas “correto formalmente” não significa necessariamente “correto matematicamente” no sentido mais amplo. A formalização pode estar correta para um enunciado sutilmente diferente do que se pensa. Essa é a nuance que os especialistas estão investigando.

Prova 2: A Hipótese do Tempo Exponencial é falsa

Essa é a bomba. Se você trabalha com computação, presta atenção.

A Hipótese do Tempo Exponencial (ETH, Exponential Time Hypothesis) é uma conjectura formulada por Russell Impagliazzo e Ramamohan Paturi em 1999. Ela afirma, simplificando: não existe algoritmo que resolva o problema 3-SAT em tempo subexponencial. Em termos práticos, a ETH diz que certos problemas computacionais são irredutivelmente difíceis, e que não há atalho significativo para resolvê-los.

A ETH não é apenas uma conjectura acadêmica. Ela é a base sobre a qual centenas de resultados de complexidade computacional foram construídos. Se a ETH é verdadeira, então vários problemas NP-completos exigem tempo exponencial. Se ela é falsa… bem, muita coisa que achávamos saber sobre a dificuldade de problemas computacionais precisa ser revisada.

O que a IA da OpenAI produziu: um algoritmo determinístico que conta exatamente o número de atribuições satisfatórias de fórmulas CNF de largura fixa em tempo subexponencial e espaço polinomial. Se isso está correto, a ETH é falsa no caso 3-SAT.

Resumo técnico:
- Problema: 3-SAT (satisfatibilidade booleana com cláusulas de 3 literais)
- Claim: existe algoritmo determinístico em tempo subexponencial
- Verificação: formalizado em Lean (17 de outubro de 2026)
- Implicação: ETH é falsa

E o P vs NP?

Calma. Todo mundo quer saber: se a ETH é falsa, isso resolve P vs NP?

Não diretamente. A ETH é uma conjectura mais forte que P ≠ NP. Refutar a ETH não prova que P = NP. O que ela faz é mostrar que problemas NP-completos podem ser resolvidos em tempo subexponencial (digamos, 2^(n^0.99) em vez de 2^n). Isso ainda é exponencial “na prática”, mas teoricamente é um avanço enorme.

Pense assim: se antes achávamos que escalar uma montanha exigia 10.000 passos, agora sabemos que dá pra fazer em 9.000. Ainda é uma montanha, mas a crença de que “não tem jeito de fazer em menos de 10.000” caiu.

Reação da comunidade

Russell Impagliazzo, Ramamohan Paturi e Ryan Williams (três dos maiores nomes em complexidade computacional) foram designados como “shepherds” do resultado. Eles publicaram uma nota dizendo explicitamente: “nosso envolvimento não deve ser interpretado como garantia de que essa afirmação é correta.”

Um pesquisador no Hacker News descreveu a situação como “possivelmente a maior surpresa em vinte anos de teoria da complexidade.” Outros foram mais cautelosos, lembrando que resultados perto dessa fronteira podem ser frágeis. Uma vírgula no lugar errado numa definição pode mudar tudo.

O que ninguém está questionando é o método de verificação. A prova foi formalizada em Lean, o que significa que cada passo lógico foi mecanicamente verificado. Se o enunciado formalizado corresponde exatamente à ETH como a comunidade a entende, a prova está correta. Esse “se” é onde mora o debate.

Prova 3: Existência da QCD em 4 dimensões

A terceira prova é a mais difícil de explicar, mas talvez a mais impressionante para físicos teóricos.

A Cromodinâmica Quântica (QCD) é a teoria que descreve como quarks e glúons interagem. É uma das peças fundamentais do Modelo Padrão da física de partículas. O problema? Ninguém nunca provou rigorosamente que a QCD existe como uma teoria matemática consistente em quatro dimensões espaço-temporais.

Essa questão faz parte dos famosos Problemas do Milênio do Instituto Clay. A formulação original pede uma prova rigorosa de existência para teorias de Yang-Mills em quatro dimensões com um “mass gap” (uma lacuna de massa positiva). O prêmio: US$ 1 milhão.

O que a IA da OpenAI produziu é uma prova de existência matematicamente rigorosa para certas teorias quânticas de campo interagentes com campos de gauge e férmions em quatro dimensões, incluindo a QCD e completions do Modelo Padrão.

David Gross (Nobel de Física 2004), Arthur Jaffe, Igor Klebanov e Nikita Nekrasov foram designados para liderar a verificação. Diferente das outras duas provas, a OpenAI reteve os materiais completos da física, impedindo auditoria externa completa. Isso gerou críticas: como validar algo que você não pode ler?

O elefante na sala: por que não nomearam o modelo?

A OpenAI não revelou qual modelo produziu essas provas. Os textos referem-se apenas a “nossos modelos” e “nosso sistema”. Não sabemos se foi o o3, o o4-mini, uma versão interna do GPT-6 com reasoning capabilities estendidas, ou algo completamente novo.

Essa opacidade é intencional. A OpenAI está claramente usando esses resultados como demonstração de capacidade, mas sem revelar a arquitetura por trás. Para uma empresa que começou com a missão de “IA aberta”, é irônico.

O que sabemos:

• As provas foram geradas em linguagem natural pelo modelo
• Depois foram formalizadas em Lean (provas 1 e 2)
• A formalização da prova 1 levou um dia
• A prova 2 foi gerada em 16 de outubro e formalizada em 17 de outubro
• A prova 3 não foi formalizada em Lean (pelo menos não publicamente)

O que isso significa pra quem escreve código

Se você é dev e está se perguntando “ok, mas o que isso muda no meu dia a dia?”, a resposta honesta é: provavelmente nada imediato. Mas no médio prazo, a refutação da ETH tem implicações práticas potenciais:

Criptografia: A ETH era usada como argumento para a segurança de certos esquemas criptográficos. Se ela é falsa, alguns desses argumentos precisam ser revisados. Isso não significa que o AES vai quebrar amanhã, mas significa que a base teórica para “isso é seguro porque é exponencialmente difícil” ficou mais fraca.

Otimização: Problemas de otimização combinatória que eram considerados “irredutivelmente difíceis” podem ter algoritmos melhores do que pensávamos. Isso afeta desde roteamento de redes até scheduling de containers em clusters Kubernetes.

Verificação de software: A formalização em Lean abre um precedente interessante. Se IAs conseguem gerar provas formais de teoremas matemáticos, elas também podem gerar provas formais de corretude de software. Imagine um mundo onde o compilador não apenas verifica tipos, mas prova que seu programa está correto.

IA para ciência: Esse é o ponto mais óbvio. Se modelos de IA conseguem superar modelos mais avançados em tarefas específicas e produzir provas que humanos não conseguiram em décadas, estamos entrando numa era onde a IA não é apenas uma ferramenta de automação (como agentes autônomos que já trabalham sozinhos), mas um motor de descoberta científica.

O precedente perigoso

Tem um lado dessa história que ninguém quer falar. A OpenAI acabou de demonstrar que modelos de IA podem produzir resultados científicos que humanos precisam de semanas ou meses para verificar. E reteve parte dos materiais.

Pense no incentivo: se uma empresa pode gerar “descobertas” mais rápido do que a comunidade consegue verificar, e se o anúncio dessas descobertas gera valor de mercado, estamos criando um sistema onde a velocidade de anúncio supera a velocidade de verificação.

A OpenAI designou “shepherds” acadêmicos para cada resultado, o que é positivo. Mas os próprios shepherds disseram que seu envolvimento não é garantia de corretude. Estamos num território novo onde a velocidade da IA na produção de resultados é incomparavelmente maior que a velocidade humana na verificação.

Isso não invalida os resultados. Pode ser que os três estejam corretos e revolucionem seus respectivos campos. Mas o processo levanta questões que vão muito além da matemática.

Lean: o juiz que não aceita suborno

Vale dedicar um momento ao Lean, porque ele é o protagonista silencioso dessa história.

Lean é um assistente de provas formais. Você escreve uma proposição matemática e uma sequência de passos lógicos, e o Lean verifica mecanicamente se cada passo segue das regras da lógica e dos axiomas. Não há espaço para “intuição” ou “parece certo”. Ou a prova está formalmente correta, ou não está.

Nos últimos anos, o Lean ganhou tração na comunidade matemática. A biblioteca Mathlib, que contém milhares de definições e teoremas formalizados, cresceu exponencialmente. Em 2023, Kevin Buzzard e colaboradores formalizaram resultados de teoria de números que antes existiam apenas em papers informais. Em 2024, Terence Tao usou Lean para verificar resultados em teoria aditiva de grupos.

O que a OpenAI fez foi usar IA para gerar provas em linguagem natural e depois traduzi-las para Lean. Esse pipeline (IA gera, Lean verifica) é novo na escala em que foi aplicado. E funciona como um sistema de checks and balances: a IA pode alucinar, mas o Lean não deixa passar.

O problema sutil é que a formalização exige traduzir conceitos matemáticos informais para definições formais. Se a tradução contiver um erro (por exemplo, se a definição formal de “3-SAT” usada no Lean for sutilmente diferente da definição padrão), a prova pode estar “correta” no Lean mas “errada” na matemática. Esse tipo de bug é raro, mas em resultados desta magnitude, é o primeiro lugar onde os revisores vão olhar.

O que vem agora

Os próximos meses vão ser decisivos. Os shepherds acadêmicos vão dissecar cada prova, e a comunidade mais ampla vai tentar encontrar falhas. Se as provas sobreviverem ao escrutínio:

• A conjectura de Kakeya, aberta desde 1917, estará resolvida
• A ETH, base de centenas de papers em complexidade, terá caído
• A existência da QCD terá sido provada, tocando num Problema do Milênio

Se alguma falha for encontrada, a OpenAI terá um problema de credibilidade. E a conversa sobre IA em ciência vai mudar de “incrível” para “perigoso” muito rápido.

Por enquanto, o Lean verificou duas das três provas. E o Lean não mente. A questão é se perguntaram a coisa certa ao Lean, ou se há uma diferença sutil entre o que foi formalizado e o que a comunidade entende por cada conjectura. Nesse gap entre formalização e interpretação é que a ciência real vai acontecer.

Três provas. Três campos. Zero garantia. A IA fez sua parte. Agora é a vez dos humanos.

Fonte de inspiração: OpenAI – Building scientific understanding with academic communities