OpenAI diz ter resolvido 3 problemas impossíveis

O gargalo não é descobrir, é provar que descobriu

Descoberta científica por IA virou o novo benchmark de prestígio. Não é mais quem tem o maior contexto ou o menor preço por token, é quem prova um teorema que estava parado há décadas ou refuta uma hipótese que todo cientista da computação assumia como verdadeira. A OpenAI acaba de entrar de cabeça nesse jogo ao anunciar três resultados grandes em matemática, ciência da computação e física, poucas semanas depois de liberar centenas de manuscritos com supostas soluções para problemas matemáticos antigos. O recado é claro: o modelo não só sugere ideias, ele gera provas completas, com formalização em Lean, prontas para verificação.

Só que quem já tentou reproduzir uma prova gerada por modelo sabe onde mora o problema real. Gerar LaTeX bonito é fácil, sustentar cada passo lógico sem furar a dependência, sem inventar lema ou esconder um salto de intuição, isso é outra história. É por isso que esse anúncio importa menos pelo número de descobertas e mais pelo novo fluxo de validação que a OpenAI está testando, com pastores acadêmicos, grupos independentes e liberação no GitHub. Se funcionar, muda como a ciência lida com resultado vindo de máquina. Se não funcionar, vira só mais uma onda de hype com equações.

O fato

A OpenAI publicou no GitHub materiais relativos a três frentes. Na matemática, um trabalho sobre suavização local para a equação de onda euclidiana, que afirma estabelecer a estimativa de Sogge para ondas em toda dimensão espacial maior ou igual a dois, com consequências para as conjecturas de Kakeya e para estimativas de restrição esférica de Stein no interior do intervalo conjecturado. Nesse caso, a empresa optou por liberar diretamente a saída do modelo, no mesmo formato da liberação de 6 de outubro, para que pesquisadores construam suas próprias explicações.

Na ciência da computação, a afirmação é ainda mais forte: a Hipótese do Tempo Exponencial seria falsa. O artigo descreve um algoritmo determinístico que conta exatamente as atribuições satisfatórias de fórmulas CNF de largura fixa em tempo subexponencial e espaço polinomial, com o caso 3-SAT refutando a hipótese original proposta em 1999. Para esse caso, a OpenAI não liberou sozinha. Um grupo independente liderado por Russell Impagliazzo, Ramamohan Paturi e Ryan Williams vai examinar e explicar a prova, com carta aberta à comunidade pedindo discussão sobre acesso antecipado, crédito e normas para breakthroughs gerados por IA.

Na física, o material ainda não foi liberado por completo. O anúncio fala em uma prova de existência matematicamente rigorosa de certas teorias quânticas de campos interativas com campos de calibre e férmions em quatro dimensões, incluindo a Cromodinâmica Quântica e uma completação unificada do Modelo Padrão. A verificação seria conduzida por um grupo liderado por David Gross, com nomes como Michael Douglas, Arthur Jaffe, Igor Klebanov e Nikita Nekrasov. É, de longe, a alegação mais sensível, porque toca em um dos problemas de fundação da física matemática.

Como funciona na visão de operador

Pense menos em chat e mais em pipeline de prova. Pelo que foi descrito, o fluxo provável é: modelo de raciocínio longo gera um rascunho em linguagem natural mais esqueleto formal, depois itera contra um verificador Lean até fechar os buracos de tipagem e de tática. O Lean aqui funciona como compilador: não aceita intuição, só aceita passo que type-check. Isso explica por que a OpenAI enfatiza tanto a prova em Lean no GitHub. Sem o artefato executável, seria só mais um PDF para debater no café. Com o artefato, qualquer laboratório pode baixar, rodar o checker e ver onde quebra.

Em termos de arquitetura, isso sugere três camadas. Primeira, geração massiva com busca e crítica interna, provavelmente com custo de inferência alto, muitas amostras, ferramentas de computação simbólica e recuperação de literatura. Segunda, formalização assistida, que é lenta e cara porque cada lema precisa ser reescrito em táticas que o kernel do Lean aceite. Terceira, validação humana distribuída, que transfere o custo de latência final para a comunidade. A OpenAI gera em horas o que levaria meses para escrever, mas a verificação ainda consome semanas de especialistas caros. A latência não sumiu, só mudou de lugar.

Não há dados públicos de custo, número de tentativas ou taxa de sucesso, então qualquer número seria chute. Mas dá para inferir o trade-off de operador: para produzir uma prova que sobreviva ao Lean, o custo de inferência por resultado válido deve ser ordens de magnitude maior que uma resposta normal. Isso só faz sentido para problemas de altíssimo valor simbólico, como ETH ou QCD, onde o retorno em reputação compensa. Não espere esse mesmo pipeline rodando barato via API amanhã para o seu problema de otimização do dia a dia.

O que muda no fluxo de publicação

O ponto novo é o modelo de pastores. Em vez de jogar o PDF no arXiv e torcer, a OpenAI entrega o output primeiro para um pequeno grupo de nomes consagrados que organizam a checagem. Para ciência da computação, isso já rendeu carta aberta e repositório público imediato a pedido do grupo. Para física, o acesso ainda é restrito. E aqui surgiu a primeira crítica relevante: o painel AGMAI de consultores em matemática, montado pela própria OpenAI, disse ontem que não recomenda essa prática de acesso antecipado para poucos, citando acesso desigual, reputação emprestada e seleção enviesada. A recomendação deles é direta: repositório acadêmico, provas formalizadas em Lean, transparência sobre como os problemas foram escolhidos, financiamento para quem faz o trabalho sujo de entender o resultado e registro de conflitos de interesse.

O que isso muda na prática

Para quem pesquisa, o recado é pragmático. Primeiro, trate todo resultado gerado por IA como pull request gigante sem revisão, não como teorema. Baixe o repositório, rode o Lean localmente, isole os lemas centrais e tente quebrar as hipóteses de contorno. Segundo, se você orienta alunos, mude o treino agora: menos memorização de truque de prova e mais leitura crítica de prova longa, depuração de tática no Lean e escrita de contraexemplos. Quem souber verificar rápido vai valer ouro nos próximos dois anos.

• Quem ganha: grupos com capacidade de verificação formal, laboratórios com cluster para rodar checkers e estudantes que dominam Lean e teoria da complexidade, porque o trabalho de simplificar e explicar vai gerar papers.
• Quem perde: quem vive de autoridade sem artefato reproduzível, periódicos lentos e qualquer narrativa de que IA vai substituir o matemático, porque o gargalo de checagem ficou ainda mais visível.
• Ação prática desta semana: clone os repositórios liberados, fixe a versão do Lean e do Mathlib, rode a prova completa e documente onde o tempo de verificação explode, esse perfil de custo é o dado mais útil que você pode publicar agora.

Para quem constrói produto com IA, a lição é outra. Prova formal é o melhor caso de uso para saída verificável por máquina, bem diferente de texto jurídico ou código sem teste. Se seu domínio tem um checker determinístico, invista nesse loop geração mais verificação, porque é onde o modelo realmente escala. Se não tem, não caia no conto de que basta aumentar o raciocínio. Sem oráculo externo, alucinação bem escrita continua indistinguível de verdade.

Tensão real: isso escala ou só move o gargalo?

Aqui está minha dúvida honesta depois de olhar o desenho. A OpenAI resolveu o problema da geração, mas terceirizou o problema da confiança para um punhado de professores famosos. Isso acelera no curto prazo, porque o nome de Gross ou Impagliazzo abre porta e atrai revisores, mas cria um ponto único de falha social. E se o pastor erra? E se o acesso antecipado permite publicar trabalho derivado com material não publicado? A carta aberta do grupo da computação tenta endereçar isso pedindo normas sobre crédito para quem checa, corrige, simplifica e estende, além de proteção para estudantes. É a pergunta certa, mas ainda sem resposta operacional.

Tem também a questão do custo de entendimento. Uma prova em Lean que passa no checker não significa uma prova que humanos entendem. A história da matemática mostra que resultado sem intuição compartilhável trava o campo em vez de destravar. Se precisarmos de seis meses e cinco pós-docs para entender cada lema gerado, o throughput real da ciência não aumentou, só empilhamos teoremas opacos. A proposta do painel AGMAI de financiar o trabalho de explicação parece chata perto do anúncio de que a ETH caiu, mas é provavelmente a parte mais importante dessa história toda.

No fim, continuo cético de forma produtiva. Quero ver o checker rodar verde na minha máquina, quero ver a simplificação independente e quero ver a comunidade reproduzir sem depender do aval inicial. Até lá, trato como hipótese forte, não como descoberta fechada. E para você que constrói ou pesquisa: a IA cientista chegou ou só aprendemos a gerar conjecturas mais convincentes e empurrar a conta da prova para os outros?