Rio de Janeiro – A startup Math Inc. anunciou que concluiu a formalização, em linguagem Lean, das demonstrações que garantiram à matemática ucraniana Maryna Viazovska a Medalha Fields em 2022. O trabalho, que resolve o problema do empacotamento de esferas nas dimensões 8 e 24, foi realizado com o apoio da inteligência artificial Gauss, desenvolvida pela própria empresa.
Como a prova foi transcrita
Segundo a Math Inc., Gauss precisou de cinco dias para converter para Lean a demonstração referente à dimensão 8. Nas duas semanas seguintes, a mesma ferramenta processou o caso da dimensão 24, baseando-se apenas no artigo original de Viazovska e buscando referências adicionais de forma autônoma. No total, foram produzidas cerca de 200 mil linhas de código Lean — volume equivalente a 10% do repositório mundial MathLib, que soma aproximadamente 2 milhões de linhas.
Histórico do problema
O estudo do empacotamento de esferas começou em 1611, quando Johannes Kepler formulou a questão motivado pelo armazenamento de balas de canhão. Em 1953, o húngaro László Tóth mostrou que o problema podia ser reduzido a um número finito, embora gigantesco, de cálculos. O norte-americano Thomas Hales declarou ter completado esses cálculos em 1998, mas o artigo, com 250 páginas e 3 GB de código, exigiu uma verificação adicional: o projeto Flyspeck, encerrado apenas em 2014, confirmou a correção da prova.
Avanços em dimensões superiores
Viazovska obteve, em 2016, a solução para a dimensão 8 utilizando propriedades específicas desse espaço. Logo depois, em parceria com outros pesquisadores, estendeu o resultado para a dimensão 24. As duas conquistas combinam técnicas de teoria dos números, geometria discreta e análise harmônica, e permanecem únicas: o problema segue em aberto para todas as demais dimensões acima de 3.
Repercussão na comunidade científica
O avanço na formalização de provas vem mudando a rotina de pesquisadores. Reportagem da revista New Scientist, publicada no fim de março, relatou que o uso de Lean revelou um erro significativo em um estudo sobre a partícula de Higgs. No Brasil, o empresário Guilherme Silveira relatou ter utilizado ferramentas de IA para obter resultados na área de geometria algébrica, tema de sua tese de doutorado.
Imagem: Internet
Diante desses episódios, especialistas apontam que a participação de sistemas automatizados na verificação de demonstrações tende a se tornar parte permanente do trabalho matemático.
Com informações de Folha de S.Paulo
