IA e o futuro da matemática: impactos e avanços

A questão do empacotamento de esferas, formulada por Kepler em 1611, busca o arranjo que maximize o número de bolas por volume no porão de navio.
Após séculos de inúmeros avanços, a prova completa ficou formalmente verificada pelo projeto Flyspeck, concluído em 2014, que confirmou a solução em dimensão tridimensional.
Em dimensões altas, surgiram avanços: em 2016, Maryna Viazovska resolveu a dimensão oito, e logo depois estendeu a prova para a dimensão vinte e quatro, com reconhecimento em 2022 pela Medalha Fields.
A startup Math Inc., liderada por Viazovska, transcreveu essas demonstrações para a linguagem Lean, tornando-as os primeiros teoremas da Medalha Fields com demonstração Verificada por Computador; Gauss, IA da empresa, liderou o esforço com milhares de linhas de código.
Em pouco tempo, Gauss gerou cerca de duzentas mil linhas de Lean, consolidando a prova de Viazovska para dimensões oito e vinte e quatro e impulsionando a relação entre IA, formalização matemática e pesquisa científica.

A marinha britânica abriu a discussão sobre como dispor balas de canhão no porão de navios para armazenar o maior número possível. Esse problema levou ao estudo do empacotamento de esferas, formulado por Johannes Kepler em 1611. A questão central é encontrar o arranjo de bolas idênticas que maximize o aproveitamento do volume.

Com o tempo, o problema ganhou escala e complexidade. Em 1953, László Tóth reduziu o desafio a um número finito de cálculos. Em 1998, Thomas Hales anunciou a conclusão desses cálculos, mas o texto era extenso demais para revisão prática. O impasse motivou um novo ciclo metodológico.

Progresso histórico

Para resolver a prova, Hales iniciou o projeto Flyspeck, transcrevendo cada passo para uma linguagem formal. O objetivo era permitir a verificação computacional rigorosa. O esforço durou mais de uma década e foi concluído em 2014, consolidando a solução do empacotamento de esferas em dimensão 3.

Em dimensões altas, novas conquistas surgiram. Em 2016, Maryna Viazovska resolveu o caso da dimensão 8 e, em seguida, ampliou a solução para a dimensão 24. Essas realizações combinaram teoria dos números, geometria discreta e análise harmônica, rendendo reconhecimento internacional e uma Medalha Fields em 2022.

Formalização por IA

Agora, a Math Inc. anunciou que uma equipe liderada por Viazovska transcreveu a prova para a linguagem Lean. A iniciativa torna os teoremas de medalha Fields formalmente verificáveis por computador. Gauss, IA especializada em formalização automática, integrou a equipe da empresa.

Gauss transformou o teorema de Viazovska em Lean em cinco dias para a dimensão 8. Em cerca de duas semanas, adaptou a abordagem à dimensão 24, baseando-se no artigo original e em pesquisas bibliográficas quando necessário. O projeto resultou em 200 mil linhas de código Lean, ampliando o acervo da MathLib.

O que vem a seguir?

A cada nova atualização, surgem desdobramentos no uso de IA para validação de teoremas. Um artigo recente sobre falhas em publicações de física ilustra o potencial da formalização para detectar inconsistências. A IA, segundo relatos, já modifica a forma como pesquisadores conduzem e validam trabalhos de matemática.