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.
Entre na conversa da comunidade