Quando a IA prova teoremas: o que sobra da profissão para os matemáticos

Google DeepMind e OpenAI criaram sistemas capazes de resolver problemas de nível olímpico e de publicar pesquisas originais de nível PhD. A comunidade matemática encara agora uma pergunta que, cinco anos atrás, parecia absurda: o que sobra para os humanos quando uma máquina prova teoremas?

A IA leva o ouro olímpico

No verão de 2024, sistemas do Google DeepMind e da OpenAI alcançaram pela primeira vez o nível dos melhores estudantes do ensino médio do mundo em matemática, ao ganhar medalhas de ouro na Olimpíada Internacional de Matemática. A competição anual pede que os participantes resolvam, em tempo limitado, seis problemas dificílimos de diferentes áreas, da teoria dos números à combinatória.

Veio então um resultado ainda mais importante: o sistema experimental da DeepMind, Aletheia, obteve sozinho resultados publicáveis de nível PhD em geometria aritmética. E um sistema da OpenAI refutou uma conjectura importante da geometria combinatória, resultado digno de um periódico matemático de primeira linha. Especialistas de destaque o chamaram de marco: pela primeira vez, a IA demonstrou pensamento independente e original, e não apenas a reprodução de métodos conhecidos.

Em paralelo, sistemas baseados em LLMs aprenderam a traduzir automaticamente demonstrações humanas para código formal em ferramentas de verificação como Lean e Isabelle. Esse processo trabalhoso antes levava meses. O sistema Gauss formalizou sozinho, em duas semanas, a demonstração do teorema do empacotamento de esferas em 24 dimensões, pela qual a matemática Maryna Viazovska recebeu a Medalha Fields.

Três posições e pavor existencial

No Fórum de Laureados de Heidelberg, em setembro de 2025, jovens matemáticos se depararam com uma imagem assustadora do futuro. Do palco, vieram previsões de sistemas de IA sobre-humanos que formularão conjecturas, construirão demonstrações e verificarão resultados sem participação humana. Yang-Hui He, do Instituto de Ciências Matemáticas de Londres, afirmou que os humanos correm o risco de virar "sacerdotes dos oráculos".

"Senti que todos ao redor estavam preocupados; eles simplesmente não tinham pensado tão longe. Foi como uma grande bomba", diz a matemática Jessica Randall, do Google Developer Groups. "Começamos a perceber que a IA é capaz de nos substituir."

Hoje, três posições se delinearam na comunidade:

• IA como ferramenta: a compreensão fica com o humano; a IA é uma calculadora avançada
• IA como parceira: humanos e máquinas resolvem juntos problemas fora do alcance de cada um isoladamente
• IA como oráculo: o que importa é obter a resposta, não importa como nem por quem

Terence Tao, medalhista Fields que ganhou ouro na olimpíada aos 11 anos, vê o futuro na "matemática grande": colaborações descentralizadas em larga escala, nas quais os humanos ficam com as partes criativas e a IA, com a rotina técnica. "Cem anos atrás, quase todo artigo saía com um único autor. No futuro, talvez eu nem saiba se foi um humano ou uma IA."

Riscos: motivação e atrofia

A primeira ameaça é a motivação. Se a IA percorre sozinha a maior parte do caminho, por que gastar anos numa luta lenta e penosa até a compreensão? Akshay Venkatesh, medalhista Fields de Princeton, admite: "Já passei anos chegando devagar à compreensão. Se um computador assume grandes partes desse trabalho, você terá motivação para mergulhar tão fundo?"

A segunda ameaça é a próxima geração. Estudantes que pulam a luta com o problema em troca de uma resposta rápida não constroem a própria intuição matemática. Com o tempo, os matemáticos correm o risco de desaprender a pensar fora das abordagens de IA com que foram formados. Por isso, a comunidade já organiza workshops, escreve ensaios e elabora regras para o uso de IA em pesquisas e publicações.

"A matemática ensina a pensar de forma lógica e racional, e isso ajuda em todos os aspectos da vida", diz

Jessica Randall.

O que isso significa

A IA não "suga a alma" da matemática: ela obriga os matemáticos a responder com honestidade por que fazem o que fazem. Pelo visto, a resposta não está em ser o primeiro a achar um resultado, mas no próprio caminho até a compreensão: uma alegria que nenhum algoritmo pode substituir nem automatizar.