Um dos teoremas mais famosos da história da matemática voltou a ocupar o centro das atenções — desta vez, com a ajuda de ferramentas de inteligência artificial. Durante um evento realizado em Londres, pesquisadores dedicados à chamada matemática formal relataram progressos inesperadamente acelerados no processo de formalização do Último Teorema de Fermat, aquela proposição enunciada no século XVII por Pierre de Fermat que afirma ser impossível encontrar três inteiros positivos capazes de satisfazer a equação aⁿ + bⁿ = cⁿ para qualquer valor de n maior que dois.
O desafio atual não é provar o teorema — isso já foi feito pelo matemático britânico Andrew Wiles em 1995, após décadas de trabalho silencioso que culminaram em uma demonstração monumental com mais de cem páginas. O que os pesquisadores buscam agora é algo distinto: traduzir essa prova para uma linguagem matemática completamente formal, verificável passo a passo por assistentes de prova computacionais como o Lean. Esse processo, conhecido como formalização, é notoriamente laborioso e exige que cada inferência lógica, por mais trivial que pareça, seja explicitada com rigor absoluto.
É aqui que a inteligência artificial entra em cena. Os modelos de linguagem de grande escala têm demonstrado uma capacidade crescente de sugerir passos intermediários, identificar lacunas na cadeia de raciocínio e até propor transformações algébricas que humanos levam horas para elaborar. No contexto do evento em Londres, essa colaboração homem-máquina produziu avanços em ritmo muito superior ao esperado, surpreendendo até os próprios organizadores. O que poderia levar meses de trabalho manual foi concluído em fração do tempo com o auxílio dos sistemas de IA.
Para a comunidade matemática, o impacto vai além do teorema em si. A formalização bem-sucedida de uma prova da complexidade de Wiles seria um marco para a área, demonstrando que a matemática contemporânea — com toda a sua sofisticação e abstração — pode ser integralmente capturada por sistemas formais auditáveis por computador. Isso abre caminho para uma nova era de verificação matemática, na qual erros sutis que passaram despercebidos por revisores humanos poderiam ser detectados automaticamente.
O episódio também alimenta um debate mais amplo sobre o papel da IA na produção científica. Não se trata de substituir o matemático, mas de amplificar sua capacidade. A intuição, a escolha dos problemas relevantes e a criatividade continuam sendo atributos humanos insubstituíveis — o que a IA oferece é velocidade, paciência e precisão nas tarefas estruturalmente repetitivas. Se o Último Teorema de Fermat sobreviveu trezentos e cinquenta anos como enigma e depois trinta como prova não formalizada, talvez esteja prestes a cruzar mais uma fronteira histórica, desta vez com um computador ao lado.