IA ajuda pela primeira vez a verificar formalmente as provas de uma vencedora da Medalha Fields

Na matemática existe um tipo de reconhecimento acima de qualquer prêmio: quando um computador confirma que a sua prova é absolutamente impecável. As provas da matemática ucraniana Maryna Viazovska, que lhe renderam a Medalha Fields em 2022, acabam de passar exatamente por esse teste, com uma participação sem precedentes da inteligência artificial.

Viazovska recebeu a medalha por resolver um dos problemas mais elegantes e traiçoeiros da matemática: o empacotamento de esferas. Parece simples: qual é a forma mais densa de dispor bolas idênticas no espaço? Em duas dimensões, qualquer apicultor sabe a resposta: o favo de mel.

Em três dimensões, o ideal é a pirâmide de bolas que todo mundo que já viu uma pilha de laranjas na feira conhece. Mas, conforme o número de dimensões cresce, o problema se torna monstruosamente complexo. Em 2016, Viazovska provou que a estrutura simétrica E8 é o melhor empacotamento no espaço de oito dimensões e, pouco depois, junto com colegas, estabeleceu que a rede de Leech é ótima em 24 dimensões.

Por mais abstratos que pareçam, esses resultados têm relação direta com os códigos de correção de erros usados por smartphones e sondas espaciais.

A comunidade matemática examinou as provas e as reconheceu como corretas, daí a Medalha Fields. No entanto, a verificação formal, processo em que um programa de computador confere cada passo lógico da prova, é uma tarefa de escala fundamentalmente diferente. Um revisor humano pode deixar passar um erro sutil; o computador, não. Por isso, a formalização de provas complexas é considerada o "padrão-ouro" de confiabilidade na matemática moderna.

Tudo começou com um encontro casual. Em Lausanne, o estudante do terceiro ano Sidharth Hariharan contou a Viazovska como usava a formalização de provas na linguagem Lean para entender a fundo conceitos matemáticos. Lean é ao mesmo tempo uma linguagem de programação e um chamado "assistente de provas", que permite escrever raciocínios matemáticos de uma forma que o computador consegue checar quanto à correção absoluta.

Viazovska se interessou e, em março de 2024, nasceu o projeto Formalising Sphere Packing in Lean. Aderiram especialistas do Imperial College London, da Universidade de East Anglia e da Universidade da Califórnia em Berkeley. A equipe criou um "blueprint", um mapa legível por humanos de todos os elementos da prova em oito dimensões, marcando quais já estavam formalizados e quais ainda precisavam ser traduzidos para Lean.

Foram dois anos de trabalho minucioso, e então veio a virada. Em outubro de 2025, a startup Math, Inc., desenvolvedora do sistema de IA Gauss, entrou no projeto. Não se trata de um modelo de linguagem comum: o Gauss é um "agente de raciocínio" capaz de alternar raciocínio em linguagem natural com dedução matemática totalmente formalizada. Na prática, é uma IA que consegue traduzir automaticamente provas matemáticas para uma linguagem que o verificador computacional entende. O Gauss acelerou radicalmente a formalização e permitiu concluir o que, de outra forma, levaria mais anos de trabalho manual.

O resultado teve forte repercussão na comunidade científica. "Esses novos resultados parecem muito, muito impressionantes e definitivamente sinalizam um progresso rápido nessa direção", disse Liam Fowl, pós-doutorando da Universidade de Princeton e especialista em raciocínio de IA, que não participou do projeto. Segundo ele, a verificação formal é uma espécie de "selo de qualidade", uma garantia absoluta de que cada passo do raciocínio lógico está correto.

A importância desse avanço vai muito além de uma única prova. Até pouco tempo atrás, formalizar resultados matemáticos relevantes dava tanto trabalho que só alguns projetos isolados se arriscavam. Se sistemas de IA como o Gauss conseguirem acelerar esse trabalho de forma sistemática, a matemática ganhará algo inédito: a possibilidade de verificar em massa provas acumuladas ao longo de décadas. Isso não substitui os matemáticos: Viazovska continua tendo realizado uma façanha intelectual que uma máquina não consegue repetir. Mas a IA se mostra insubstituível na parte mais rotineira e crítica do trabalho: conferir que a intuição genial não levou a um erro em algum dos milhares de passos lógicos.

Estamos vendo o nascimento de um novo modelo de colaboração: o humano formula as ideias e constrói as provas, e a máquina garante que elas são impecáveis. Para uma área em que um único erro despercebido pode colocar em dúvida décadas de pesquisas posteriores, isso é mais do que uma comodidade: muda a forma de trabalhar da disciplina.