OpenAI diz ter provado Kakeya, mas esconde a prova

O problema não é a descoberta, é a checagem

OpenAI diz que resolveu três dos problemas mais duros da ciência moderna e ao mesmo tempo decide quem pode ver o quê, quando e como. Para quem constrói com IA, isso é o pior cenário possível. Não porque o resultado seja falso, mas porque ele é inverificável na prática. Você tem um claim gigante sobre a conjectura de Kakeya, sobre a exponential time hypothesis e sobre cromodinâmica quântica, mas recebe apenas um output parcial, um anúncio de grupo externo e, no caso da física, nada além da promessa de que especialistas vão decidir depois. É ciência ou é demo controlada por RP?

O fato

A empresa anunciou na segunda-feira avanços em matemática, ciência da computação e física, com uma estratégia diferente de divulgação para cada um. Na matemática, afirma ter resolvido a conjectura de Kakeya em todas as dimensões, que em termos simples pergunta qual é o menor espaço necessário para girar uma agulha em todas as direções. A versão em três dimensões rendeu neste ano uma Medalha Fields para Hong Wang, da NYU, o que dá a dimensão do tamanho do claim. A OpenAI liberou o output gerado por IA e uma formalização em Lean, deixando para a comunidade a tarefa de organizar a explicação e a verificação.

Na ciência da computação, o claim é ainda mais agressivo. A empresa diz ter refutado a exponential time hypothesis, uma suposição central de que certos problemas não podem ser resolvidos muito mais rápido que força bruta, com ligação direta com o P versus NP, um dos problemas do Prêmio do Milênio. Aqui a liberação foi ainda mais restrita. A OpenAI disse que vai montar um grupo externo para explicar o resultado. Na física, a situação é pior. O trabalho toca a cromodinâmica quântica e a teoria de Yang-Mills, base do Modelo Padrão e também ligada a outro problema do Milênio, sem resolver o famoso mass gap. Esse material não foi publicado. A empresa disse que vai deferir a decisão para especialistas externos sobre como e se liberar.

Como funciona na visão de quem opera

Para entender o que está em jogo, esqueça por um minuto o brilho do enunciado e olhe para o artefato. Em matemática, o único objeto realmente auditável até agora é a formalização em Lean. Lean não é um PDF bonito, é código que um verificador consegue checar passo a passo. O matemático Brendan Hassett, da Brown, disse que o claim parece bem sustentado, mas fez a ressalva óbvia. Ele ainda não checou a formalização em Lean. Esse detalhe importa porque é aí que mora o custo real. Verificar uma prova longa em Lean exige ambiente reproduzível, versão do Mathlib travada, tempo de CPU considerável e gente que saiba ler tática por tática. Não é apertar um botão, é rodar um pipeline pesado e depurar onde ele quebra.

O que a OpenAI provavelmente fez, por inferência técnica plausível, foi combinar geração massiva de candidatos a prova com busca orientada e verificação formal como filtro. Isso é consistente com o despejo de centenas de preprints no início de outubro que deixou matemáticos exaustos. Você gera milhares de esboços, usa o verificador para podar, itera com modelo crítico e só no final humaniza o que passou. Arquiteturalmente faz sentido. É um loop de gerador e verificador, com Lean ou outro solver como ground truth parcial. Onde não há verificador automático forte, como em física teórica, o loop fica manco. Talvez por isso a física não foi liberada. Sem âncora formal, o risco de vazar um argumento com buraco sutil é muito maior.

Pense em custo e latência como operador. Gerar esse volume de provas não é uma chamada de API barata. Envolve clusters grandes, muitas tentativas, reranking e formalização, que é a parte mais cara e lenta. Depois o custo inverte e cai no colo da comunidade. Cada grupo de pesquisa precisa gastar semanas de pós-doc e horas de cluster para tentar reproduzir. A latência de verificação é medida em meses, não em tokens por segundo. Quando a empresa controla o gating, ela controla também a fila de verificação. Quem é chamado para o grupo de 'shepherds' verifica primeiro, publica primeiro, orienta a narrativa. Quem está fora espera sobra de material e tenta adivinhar hiperparâmetros no escuro.

O que isso muda na prática

Quem ganha agora é quem já vive dentro do ecossistema de prova assistida. Grupos com pipeline de Lean rodando, com CI para formalização e gente treinada em teoria geométrica da medida ou complexidade vão surfar primeiro. Laboratórios de IA com acesso a modelos internos da OpenAI também ganham, porque podem testar variações do método gerador-verificador nos seus próprios problemas. Quem perde é o pesquisador médio, o professor sem cluster grande, o aluno que queria apenas ler a prova em linguagem humana e aprender com ela. A ciência aberta perde ritmo porque a verificação vira privilégio, não protocolo.

• Rode o artefato Lean em ambiente isolado antes de opinar sobre Kakeya, trave dependências e registre onde a checagem falha.
• Monte um reading group focado em refutação para a parte de complexidade, tentando quebrar a refutação da ETH em vez de apenas aplaudir.
• Trate o anúncio de física como indisponível para roadmap, não pause experimentos nem mude tese por causa de claim sem material.

Na prática, a ação imediata para times que constroem com IA é simples. Se você usa LLMs para matemática, código ou raciocínio formal, replique o padrão gerador mais verificador no seu domínio. Não espere o modelo da OpenAI explicar tudo. Coloque um verificador barato no loop, seja teste unitário, Lean, solver SMT ou simulador físico, e meça taxa de prova que passa sem intervenção humana. Para times de produto, a lição é não ancorar narrativa em breakthrough fechado. Se sua startup depende de que a ETH caiu ou de que Yang-Mills foi simplificado, você não tem roadmap, tem aposta.

A tensão que ninguém quer encarar

Aqui está a dúvida real que fica depois do hype. Isso escala como ciência ou só move o gargalo de lugar? Antes o gargalo era criar a ideia da prova. Agora, com geração massiva, o gargalo vira verificação humana e capacidade de ler Lean por horas. A OpenAI gerou centenas de preprints em outubro e agora mais três resultados enormes, mas a comunidade tem o mesmo número de especialistas, o mesmo tempo e o mesmo orçamento. Jogar mais outputs no sistema sem liberar método, dados de treino, scripts de busca e logs de formalização não acelera a ciência, congestiona. É como aumentar throughput de escrita sem aumentar throughput de leitura.

E tem o ponto do custo que compensa para quem. Para a OpenAI, gatekeeping faz sentido corporativo. Ela protege vantagem competitiva na corrida pela AGI, evita ser refutada em público rápido demais e escolhe aliados acadêmicos que vão contar a história do jeito certo. Para a ciência, é corrosivo. A frase que circulou entre pesquisadores resume tudo. Não faz sentido que só alguns cientistas ilustres possam olhar primeiro. Se o método é robusto, por que não liberar tudo de uma vez com reprodução em um clique. Se não é robusto, por que anunciar como breakthrough em três áreas de uma vez. Ou a empresa confia no verificador e abre, ou não confia e deveria segurar o anúncio.

Conclusão

No fim, temos claims enormes, artefatos parciais e um processo de divulgação sob medida que mais confunde do que esclarece. A pergunta que fica para quem opera é direta. Você vai desenhar seu trabalho assumindo que essas provas estão certas, ou vai exigir reprodução antes de mudar qualquer linha do seu roadmap?