AI ajudou a verificar formalmente, pela primeira vez, as demonstrações de uma laureada com a Medalha Fields

Na matemática, existe um tipo especial de reconhecimento que fica acima de qualquer prêmio: quando um computador confirma que sua demonstração é absolutamente impecável. As demonstrações da matemática ucraniana Marina Viazovska, que lhe renderam a Medalha Fields em 2022, acabam de passar por exatamente tal verificação — e fizeram isso com participação sem precedentes da inteligência artificial.

Viazovska recebeu sua medalha por resolver um dos problemas mais elegantes e traiçoeiros da matemática — o problema do empacotamento de esferas. Parece simples: como você posiciona bolas idênticas no espaço da forma mais densa possível? Em duas dimensões, todo apicultor conhece a resposta — favos de mel.

Em três dimensões, uma pirâmide de esferas é ótima, familiar para qualquer um que tenha visto uma pilha de laranjas na prateleira. Mas conforme o número de dimensões aumenta, o problema fica extraordinariamente complexo. Em 2016, Viazovska provou que a estrutura simétrica E8 é o empacotamento ideal no espaço oito-dimensional, e logo depois, junto com colegas, estabeleceu que a rede de Leech é ótima em 24 dimensões.

Apesar de sua aparente abstração, esses resultados têm relevância direta para códigos com correção de erros usados por smartphones e sondas espaciais.

A comunidade matemática verificou e reconheceu as demonstrações como corretas — daí a Medalha Fields. Contudo, a verificação formal — um processo no qual cada passo lógico da demonstração é verificado por um programa de computador — é uma tarefa de escala fundamentalmente diferente. Um revisor humano pode passar por cima de um erro sutil, um computador não consegue. É por isso que a formalização de demonstrações complexas é considerada o "padrão ouro" de certeza na matemática moderna.

Tudo começou com um encontro casual. Em Lausana, um estudante do terceiro ano Siddharth Hariharan contou a Viazovska como ele usava formalização de demonstrações na linguagem Lean para uma compreensão mais profunda de conceitos matemáticos. Lean é simultaneamente uma linguagem de programação e o chamado "assistente de demonstrações", permitindo registrar raciocínios matemáticos em uma forma que um computador pode verificar com correção absoluta.

Viazovska se interessou, e em março de 2024, nasceu o projeto Formalising Sphere Packing in Lean. Juntaram-se a ele especialistas do Imperial College Londres, Universidade de East Anglia e Universidade da Califórnia em Berkeley. A equipe criou um "esboço" — um mapa legível para humanos de todos os elementos da demonstração oito-dimensional, marcando quais já tinham sido formalizados e quais ainda precisavam ser traduzidos para Lean.

Dois anos de trabalho laborioso — e então ocorreu um avanço. Em outubro de 2025, a startup Math, Inc., que desenvolveu o sistema de IA Gauss, se juntou ao projeto. Isso não é um modelo de linguagem comum: Gauss é um "agente de raciocínio", capaz de alternar entre raciocínio em linguagem natural e inferência matemática completamente formalizada. Essencialmente, é uma IA que consegue traduzir automaticamente demonstrações matemáticas em uma linguagem compreensível a um verificador de computador. Conectar Gauss acelerou dramaticamente o processo de formalização, permitindo a conclusão do que de outra forma levaria ainda anos de trabalho manual.

O resultado ressoou significativamente na comunidade científica. "Estes novos resultados parecem muito e muito impressionantes e certamente sinalizam progresso rápido nesta direção", observou Liam Foul, pós-doutorado da Universidade de Princeton e especialista em raciocínio de IA, que não participou do projeto. Segundo ele, verificação formal é uma espécie de "selo de qualidade", uma garantia absoluta de que cada passo de raciocínio lógico está correto.

O significado deste avanço vai muito além de uma única demonstração. Até recentemente, a formalização de resultados matemáticos sérios era um processo tão trabalhoso que apenas projetos isolados se arriscavam nele. Se sistemas de IA como Gauss conseguirem acelerar sistematicamente este trabalho, a matemática ganhará algo sem precedentes: a capacidade de verificar em massa demonstrações acumuladas ao longo de décadas. Isso não é uma substituição para matemáticos — Viazovska ainda realizou um feito intelectual que as máquinas não conseguem replicar. Mas a IA se prova indispensável na parte mais rotineira e crucial do trabalho — verificar que a intuição brilhante não levou a um erro em um dos milhares de passos lógicos.

Estamos testemunhando o nascimento de um novo modelo de colaboração: humanos formulam ideias e constroem demonstrações, enquanto máquinas garantem sua impecabilidade. Para a matemática, onde um erro não percebido pode lançar dúvida sobre décadas de pesquisa subsequente, isso não é meramente conveniente — é uma mudança de paradigma.