O problema não é a IA acertar, é ninguém conseguir conferir

Provas geradas por IA viraram o novo gargalo da matemática. Imagine abrir um manuscrito de 40 páginas, cheio de passos logicamente encadeados, notação estranha, saltos que parecem óbvios para a máquina, mas que para você não fazem sentido. Você chama um colega, ele também trava. Você joga o texto em outra IA para explicar e recebe uma explicação confiante, mas que você não consegue auditar. Foi exatamente isso que aconteceu quando a OpenAI despejou de uma vez mais de 700 arquivos com supostas soluções para problemas matemáticos em aberto.

Para quem constrói com modelos de linguagem, a cena é familiar. Gerar é fácil, validar é doloroso. A matemática só escancarou o problema porque lá a validação é tudo. Sem verificação humana independente, uma prova não vale nada, mesmo que o resultado final esteja correto. É essa tensão que fez a Association for Human Mathematics pedir boicote formal à OpenAI e que colocou nomes como Terence Tao e Scott Aaronson no centro de uma briga que vai muito além de vaidade acadêmica.

PublicidadeAnuncie aqui336x280 / responsivo

O fato: 700 arquivos, um boicote e dois pesos pesados

O estopim foi direto. A OpenAI publicou em lote centenas de manuscritos matemáticos produzidos por um modelo interno, afirmando ter resolvido mais de 100 problemas em aberto em um único mês, incluindo uma abordagem para o problema do milênio de Navier-Stokes. A Association for Human Mathematics, que tem Terence Tao como presidente, respondeu com um chamado público para que matemáticos parem de colaborar com a empresa.

O argumento central é simples e incômodo. A associação diz que matemáticos não pediram esse trabalho, que o lançamento massivo não foi um gesto acadêmico, mas uma demonstração de força. O texto ainda cutuca as disputas de direitos autorais que a OpenAI enfrenta no mundo todo, sugerindo que esses resultados só existem porque o modelo foi treinado sobre o trabalho de anos da própria comunidade, com ou sem autorização clara. Scott Aaronson resumiu o clima no blog dele como um 'Mathocalypse', um apocalipse da matemática onde soluções aparecem mais rápido do que qualquer humano consegue ler.

O caso Navier-Stokes piorou tudo. Pouco antes de dois matemáticos apresentarem uma solução assistida por IA feita com ajuda do ChatGPT, a OpenAI anunciou a própria solução para o mesmo problema. Vieram suspeitas de que dados da conversa teriam sido usados no treinamento, algo que a empresa nega. Para completar, a OpenAI havia criado um grupo consultivo no Institute for Advanced Study para orientar o uso de IA em matemática avançada, mas esse grupo não tem poder real sobre o ritmo da pesquisa interna. Na prática, o conselho aconselha, a empresa corre na frente e a comunidade fica com o trabalho de limpar a bagunça.

Como funciona: gerar prova é barato, validar é caríssimo

Do ponto de vista de operador, o que a OpenAI fez é tecnicamente plausível e operacionalmente brutal. Um modelo de raciocínio longo, provavelmente com busca, verificação formal parcial e pós-processamento para LaTeX, consegue cuspir candidatos a prova em escala. O custo de inferência para gerar 700 rascunhos é alto, mas diluído e paralelizado em GPUs, vira um lote gerenciável para um laboratório desse porte. O problema está na outra ponta do pipeline.

Uma prova matemática não é como um texto de marketing que você aprova no olho. Ela exige checagem linha a linha, reconstrução de intuições, conexão com literatura anterior e, cada vez mais, formalização em assistentes como Lean ou Coq. A latência aqui não é de API, é humana. Um especialista pode gastar semanas para validar um único resultado denso. Quando o texto vem com estilo estranho, com lemas mal nomeados, com referências incompletas e com passos que só fazem sentido no espaço latente do modelo, esse tempo explode. É por isso que até medalhistas Fields estão precisando de IA para tentar decifrar provas feitas por IA, entrando em um loop de confiança que a matemática tradicional nunca aceitou.

Minha inferência técnica, e deixo claro que é inferência, é que a OpenAI priorizou cobertura sobre legibilidade. É o comportamento típico de otimização para taxa de resolução em benchmark interno, não para clareza pedagógica. O modelo provavelmente foi recompensado por chegar a um verificador final ou a um juiz interno, não por produzir uma narrativa que um humano de pós-doutorado consiga seguir. Isso explica o volume e a opacidade. Também explica por que a comparação com a Anthropic incomodou tanta gente. No caso citado por Aaronson, a Anthropic trabalhou com dois pesquisadores, pagou pelo trabalho e publicou uma versão legível da refutação de duas conjecturas antigas. Menos escala, mais responsabilidade editorial. A OpenAI fez o oposto, jogou os rascunhos crus no colo da comunidade e terceirizou de graça o trabalho mais chato e mais importante.

O que isso muda na prática

Quem ganha no curto prazo são os times com infraestrutura para filtrar esse entulho. Laboratórios bem financiados, grupos com acesso a clusters e a modelos fortes conseguem garimpar ideias úteis no meio do ruído. Quem perde é o pesquisador médio, o revisor voluntário, o estudante que precisa entender o porquê, não só o quê. Se resolver virar commodity e entender continuar escasso, a matemática corre o risco de virar mineração, onde poucos extraem e muitos ficam tentando validar migalhas sem crédito, sem pagamento e sem citação adequada.

  • Ação prática para quem usa IA hoje: se você gera código, provas, relatórios técnicos ou análises com LLM, mude seu pipeline agora, exija saída em duas camadas, uma formal para máquina checar e outra narrativa para humano auditar.
  • Na prática: force o modelo a citar fontes, explicitar lemas, separar o que é conjectura auxiliar do que está provado e rodar checagem automática antes de publicar qualquer coisa.
  • Regra de ouro: se nem você consegue explicar o que o modelo fez em uma reunião de 15 minutos, não publique como resolvido, publique como rascunho para revisão.

Para empresas que operam agentes de pesquisa, a lição é sobre custo total. Você pode reduzir o custo por solução gerada em 10 vezes e ainda assim quebrar a operação, porque o custo por solução validada dispara. Latência humana não escala com mais GPUs. Sem camada de humanização, curadoria e atribuição correta, você só move o gargalo da geração para a verificação e ainda queima a confiança da comunidade que você precisa para validar.

A tensão que ninguém quer encarar

Aqui está a dúvida real que Tao e outros 24 medalhistas Fields levantaram. Resolver problemas é o objetivo da matemática ou só uma ferramenta para criar entendimento conceitual. Se a IA resolver tudo em lote, mas ninguém absorver as ideias novas, a área avançou ou só produziu troféus. O manifesto deles fala em desalinhamento severo e alerta que despejar soluções pode destruir terreno fértil em vez de gerar ideias novas. Isso dói porque é verdade também em software, em ciência de dados, em produto. Quantas vezes um agente cospe uma solução que funciona, mas o time não aprende nada e fica refém na próxima mudança.

E tem o lado feio da atribuição. Anúncios apressados sem revisão adequada, sem citação do trabalho anterior, sem crédito para quem manteve a base viva por décadas. Quando 700 arquivos caem de uma vez, quem vai rastrear plágio, redescoberta ou contaminação de dados. A acusação velada de que modelos treinam sobre papers sem licença e depois competem com os próprios autores não vai sumir. Ela vai crescer, porque o incentivo econômico é exatamente esse, sugar o conhecimento comum e privatizar a descoberta. O modelo da Anthropic de eleger emissários pagos resolve parte disso, mas cria outro problema, uma empresa privada escolhendo quais matemáticos ganham visibilidade. Nenhum dos dois modelos está pronto. Um socializa o custo da validação, o outro privatiza o prestígio da descoberta.

Conclusão

No fim, a OpenAI provou que consegue gerar matemática em escala industrial, mas não provou que isso é fazer matemática. Enquanto a verificação continuar humana, lenta e cara, jogar volume no sistema sem legibilidade é só transferir trabalho. Será que aceitamos contar como resolvido aquilo que nenhum humano ainda conseguiu entender de verdade.