Até poucos meses atrás, a matemática operava num ritmo que qualquer equipe de engenharia reconheceria: um pesquisador dedicava anos a um problema, redigia a demonstração, submetia a um periódico e esperava meses, às vezes mais, pela revisão por pares. A produção era lenta e a checagem era lenta, e o sistema se sustentava porque as duas velocidades eram comparáveis. No dia 6 de outubro de 2026, a OpenAI (abre em nova aba) rompeu esse equilíbrio de forma deliberada: publicou de uma só vez centenas de resultados matemáticos gerados por um modelo interno, acompanhados de um texto de divulgação com o título "Symmetric Cryptography and the Next 100 Years of Mathematics". A resposta da comunidade variou do assombro ao pedido formal de boicote, e o motivo da tensão interessa a qualquer profissional que dependa de verificação, auditoria ou reprodução de resultados computacionais.
O que caiu na rede
As contagens divergem entre as coberturas, e a divergência em si já é informativa. Uma das reportagens descreve 722 manuscritos organizados em 372 famílias de resultados relacionados, publicados no GitHub; reportagens baseadas no anúncio da empresa falam em 377 problemas abordados. A diferença provavelmente reflete critérios de agrupamento distintos, mas o essencial é consistente em todas as fontes: um volume de dezenas de milhares de páginas cobrindo álgebra, teoria dos números, topologia, lógica matemática e ciência da computação teórica, produzido por um modelo que a OpenAI não liberou ao público.
Três números técnicos ajudam a dimensionar o feito. Segundo a empresa, cada resultado consumiu em média o equivalente a cerca de três horas de raciocínio no ChatGPT Pro, num processo que avaliou cerca de quatro mil problemas. Muitas das demonstrações foram checadas no Lean (abre em nova aba), um assistente de provas que verifica mecanicamente se cada passo segue as regras da lógica. E apenas dez dos resultados vieram acompanhados de resumos explicando como o modelo chegou à resposta.
O lançamento não foi um evento isolado. A OpenAI acumulou anúncios ao longo de 2026: segundo uma das coberturas, um modelo interno teria refutado em maio uma conjectura de Paul Erdős formulada em 1946; em setembro, a empresa anunciou um avanço nas equações de Navier-Stokes, um dos Problemas do Milênio, abertos há cerca de nove décadas e dotados de recompensa de US$ 1 milhão. Esse anúncio anterior já era alvo de ceticismo, e a nova leva de resultados o transformou em pauta geral.
O que o Lean garante, e o que continua humano
Para quem trabalha com software, a melhor analogia para o Lean é a diferença entre um compilador e uma revisão de código. O Lean, baseado em teoria dos tipos dependentes, exige que cada inferência de uma demonstração seja reduzida a passos que o verificador aceita ou rejeita. Uma prova que passa no Lean não contém erros formais, do mesmo modo que um programa que compila não contém erros de tipo.
A checagem formal, porém, cobre apenas uma dimensão da validação matemática. Ela confirma que a lógica está correta, mas não diz se o resultado é novo, se resolve o problema que afirma resolver, se a técnica é interessante ou se a demonstração é compreensível. Isso segue sendo trabalho humano, e é justamente aí que a avalanche cria tensão: dezenas de milhares de páginas mecanicamente corretas, mas inéditas, precisam ser lidas, situadas na literatura e avaliadas quanto à relevância por pesquisadores que não participaram da produção. O verificador resolveu o problema da correção e transferiu todo o resto para uma fila que não cresceu.
O modelo que ninguém pode executar
Há uma segunda camada do problema, mais familiar a desenvolvedores: a irreprodutibilidade. O modelo que gerou as provas é interno e não foi liberado, o que impede que outros pesquisadores testem o sistema nas mesmas condições ou tentem reproduzir o processo que levou às respostas. É o equivalente a publicar os artefatos de saída de um experimento sem publicar o código que os produziu.
A OpenAI diz que trabalha para liberar o modelo de forma responsável e que pretende detalhar mais as próximas publicações. Também houve um esforço institucional real de governança: a divulgação seguiu recomendações do Advisory Group on Mathematics and Artificial Intelligence, grupo consultivo sediado no Institute for Advanced Study, em Princeton, que inclui nomes como Timothy Gowers e Edward Witten. Entre as recomendações públicas do grupo está a divulgação de todos os comandos enviados aos agentes de IA e de suas cadeias de raciocínio. Publicar dez resumos explicativos para centenas de resultados fica visivelmente aquém dessa diretriz, e o próprio grupo reconheceu em comunicado que a publicação marca "o início, e não a conclusão" de um processo que pode levar anos.
Da euforia ao boicote
As reações registradas até agora cobrem todo o espectro. O cientista da computação Scott Aaronson batizou o momento de "Mathocalypse" e o descreveu como um dos maiores dias da história da matemática. Alex Kontorovich, chefe do departamento de matemática da Universidade Rutgers, está entre os que avaliam o material. Bryna Kra, ex-presidente da Sociedade Americana de Matemática, classificou os resultados como impressionantes, mas foi direta sobre o processo: "A revisão por pares deixou de existir nesse processo". Segundo a Folha, um francês ganhador da Medalha Fields observou que a IA pode reduzir o prazer da descoberta.
No extremo da reação negativa, a Association for Human Mathematics criticou a publicação em massa, pediu que matemáticos deixem de colaborar com a OpenAI e argumentou que a área "não pediu" por esse tipo de produção. As críticas concretas citadas nas coberturas combinam três elementos: a ausência de revisão por pares antes da divulgação, o fato de o modelo ser privado e o risco de a profissão ser redefinida por decisões corporativas tomadas fora dela. Já segundo o líder de pesquisa da OpenAI, Dan Roberts, os testes internos em problemas abertos são necessários para desenvolver melhores ferramentas, e as demonstrações surgiram como subproduto desse processo de avaliação.
Há ainda o alarme de segurança. O título da própria divulgação, que menciona criptografia simétrica e os próximos cem anos da matemática, conecta o episódio a uma preocupação antiga da área: problemas de teoria dos números e complexidade computacional sustentam esquemas criptográficos em uso comercial. O medo expresso por parte dos pesquisadores é que avanços nesse território, produzidos em privado e divulgados em massa, alterem o cálculo de risco de sistemas que protegem a infraestrutura da internet antes que a comunidade consiga avaliá-los. Trata-se de uma hipótese de trabalho, não de um efeito demonstrado, mas é a hipótese que dá peso econômico ao debate.
O gargalo mudou de lugar
A leitura mais útil para profissionais técnicos não está no número de teoremas, e sim na mudança estrutural que o episódio evidencia. Quando a geração de demonstrações se torna barata, o recurso escasso deixa de ser a prova e passa a ser a verificação compreensiva: saber o que o resultado significa, se é novo e se importa. A composição de valor se desloca de quem produz para quem valida, curadoria e contextualiza. É o mesmo movimento já visto em áreas como geração de código, onde ferramentas que produzem volume elevaram o preço relativo de quem revisa.
Para times de engenharia, o sinal concreto é o do ecossistema de verificação formal. Se modelos de IA conseguem produzir demonstrações checáveis em Lean, a fronteira se desloca também para software: provas formais de propriedades de programas, até hoje restritas a nichos como kernels de sistemas operacionais e compiladores verificados, tendem a ficar mais baratas de produzir. Quem trabalha com sistemas críticos, protocolos criptográficos ou compliance tem motivo prático para acompanhar ferramentas dessa família, independentemente do desenlace da polêmica com a OpenAI.
O detalhe que resume o impasse é pequeno diante do volume: de 722 manuscritos, apenas dez vieram com explicação do raciocínio que os produziu. O resto está lá, público, gratuito e em inglês, esperando que humanos descubram o que a máquina fez.
Perguntas frequentes
Os resultados divulgados pela OpenAI já foram validados pela comunidade matemática?
Não. Parte das demonstrações passou por checagem mecânica no Lean, que confirma a correção lógica dos passos, mas a análise humana de novidade e relevância está apenas começando. O grupo consultivo do IAS estimou que a verificação completa pode levar anos, e a revisão por pares tradicional não ocorreu antes da divulgação.
O que é o Lean e qual o papel dele nessa história?
Lean é um assistente de provas baseado em teoria dos tipos dependentes: ele verifica mecanicamente se cada passo de uma demonstração segue as regras da lógica. Ele garante que uma prova não contém erros formais, mas não avalia se o resultado é novo, importante ou bem compreensível.
O modelo que gerou as provas pode ser testado por pesquisadores externos?
Não. A OpenAI usou um modelo interno ainda não liberado, o que impede testes nas mesmas condições e a reprodução do processo. A empresa afirma que trabalha para liberar o modelo de forma responsável, mas não divulgou prazo.
Como pesquisadores brasileiros podem acessar o material divulgado?
Os manuscritos estão publicados no GitHub, em acesso público e gratuito, com conteúdo em inglês. Qualquer pesquisador pode baixar os textos e reexecutar as checagens no Lean; o que não é possível, por enquanto, é executar o modelo que os produziu.