No que só pode ser descrito como o equivalente acadêmico de deixar cair um piano na cabeça de alguém e depois pedir que essa pessoa revise a partitura, a OpenAI lançou esta semana quase 400 resultados matemáticos gerados por IA, distribuídos por mais de 700 manuscritos. A reação da comunidade matemática variou de "estonteante" a "pura insanidade" — e esses foram os educados.

A coleção abrange combinatória, vários ramos da geometria, teoria dos números, ciência da computação teórica, álgebra, topologia, probabilidade e mecânica estatística, e física matemática. É tão vasta que a OpenAI se sentiu compelida a publicar orientações sobre como navegar pelo extenso repositório no GitHub, o que é um pouco como entregar a alguém um mapa de um prédio que você acabou de incendiar.

"Só passar pela lista inteira de resumos é esmagador", disse Álvaro Lozano-Robledo, professor de matemática na Universidade de Connecticut. Vários matemáticos disseram ao The Verge que simplesmente percorrer o índice de cerca de 40 páginas e os resumos levou a maior parte de uma hora. Para quem está contando em casa, isso é uma hora só para ler o cardápio.

Espalhadas entre as centenas de manuscritos estão formalizações em Lean, uma linguagem de programação e assistente de provas que permite que resultados sejam verificados computacionalmente. Essas formalizações provaram ser instrumentais para avaliar algumas das alegações matemáticas anteriores da OpenAI, dando aos pesquisadores confiança de que uma afirmação é logicamente correta mesmo que não entendam completamente o argumento por trás dela — o que é um pouco como confiar em uma calculadora sem saber o que é divisão.

Mas o grau em que cada resultado foi verificado variava enormemente. No GitHub, a OpenAI reconheceu que os resultados estão "em diferentes estágios de verificação" e que "muitos, mas não todos, dos manuscritos foram formalizados". No momento da escrita, menos da metade dos manuscritos da coleção parece ter sido descrita formalmente. A OpenAI disse que apenas 300 resultados principais dos 719 manuscritos haviam sido formalizados — cerca de 42% — e que "atualizará o repositório com mais formalizações à medida que as obtivermos". Então, aproximadamente 58% do apocalipse matemático permanece não verificado. Durma bem.

Vários matemáticos reclamaram ao The Verge da falta de formalização, particularmente dado o número enorme de resultados. Mesmo quando o código Lean acompanha um resultado, a avaliação não é instantânea. Os pesquisadores precisam verificar se a formalização realmente prova o que o resultado afirma — outro processo demorado. Vários que examinaram os artigos disseram que, mesmo onde provas verificáveis por computador foram fornecidas, a qualidade era inconsistente e as declarações que elas verificavam nem sempre pareciam corresponder perfeitamente às alegações nos manuscritos que as acompanhavam.

Kevin Buzzard, professor de matemática no Imperial College London, disse ter identificado numerosos teoremas em sua área de trabalho — teoria algébrica dos números — dos quais apenas cerca de seis imediatamente "se destacaram". Poucos, se algum, desses pareciam estar formalmente verificados em Lean. "Portanto, ou eu tenho que ler lixo possivelmente incorreto, ou esperar que outros façam o mesmo, ou esperar que alguém os formalize antes que eu possa dizer com certeza que os resultados são sequer corretos." As preocupações de Buzzard foram ecoadas por vários outros pesquisadores, que presumivelmente tinham outras coisas para fazer esta semana.

Buzzard estava longe de ser o único preocupado com o "lixo" da IA — uma abreviação para material gerado por IA de baixa qualidade e frequentemente errôneo que cada vez mais aparece online e no mundo real, incluindo artigos acadêmicos. Como em outras áreas, matemáticos disseram ao The Verge que viram um enorme aumento de tal material produzido com ferramentas como ChatGPT e Claude nos últimos anos. Muito disso é confuso, difícil de ler e demonstra pouco entendimento do assunto; é especialmente ruim quando se trata de creditar outros pesquisadores. Os escritos matemáticos anteriores da OpenAI foram amplamente criticados por especialistas por