Como dispor balas de canhão no porão do navio de tal modo que caiba o maior número possível? Essa preocupação prática da marinha britânica deu origem ao problema matemático do empacotamento de esferas, formulado pela primeira vez em 1611 por Johannes Kepler: qual arranjo de bolas (idênticas) permite armazenar mais bolas por unidade de volume?

Kepler acreditava que a resposta seria o empacotamento hexagonal em camadas, que é justamente o modo como laranjas costumam ser exibidas na feira. Mas ele não sabia provar, e praticamente não houve progresso até meados do século 20.

Em 1953, o húngaro László Tóth reduziu o problema a um número finito (mas enorme!) de cálculos. Em 1998, o norte-americano Thomas Hales anunciou ter completado esses cálculos. Mas seu artigo era muito longo (250 páginas mais 3 gigabytes de código): os especialistas responsáveis por revisá-lo jogaram a toalha após quatro anos de trabalho.

Para acabar com as dúvidas, no ano seguinte Hales lançou o projeto Flyspeck: durante mais de uma década, uma equipe de matemáticos transcreveu todos os passos da prova para uma linguagem formal, de modo que pudessem ser verificados rigorosamente por computador. O trabalho só terminou em 2014, mas foi conclusivo: os raciocínios estão corretos e, portanto, o problema do empacotamento de esferas em dimensão 3 está definitivamente resolvido.

Matematicamente, o problema faz sentido em qualquer dimensão e, curiosamente, os avanços seguintes vieram em dimensões altas.

Em 2016, a ucraniana Maryna Viazovska usou uma propriedade específica da dimensão 8 para resolver a questão nessa dimensão. Logo depois, juntamente com colaboradores, ela estendeu a prova para a dimensão 24. São façanhas impressionantes, combinando ideias sofisticadas de teoria dos números, geometria discreta e análise harmônica. Por esses resultados, Viazovska ganhou a medalha Fields em 2022. O problema continua em aberto em todas as outras dimensões maiores do que 3.

Agora, a startup Math Inc. acaba justamente de anunciar que uma equipe liderada pela própria Viazovska conseguiu transcrever a prova desses resultados para a linguagem Lean, tornando-os os primeiros teoremas “medalha Fields” a terem suas demonstrações verificadas formalmente por computador. E um protagonista desse projeto é Gauss, a inteligência artificial especializada em formalização automática da Math. Inc..

Após lidar com diversos resultados auxiliares, Gauss transcreveu o teorema de Viazovska em dimensão 8 para Lean em apenas 5 dias. Em seguida, no espaço de duas semanas, tratou do caso de dimensão 24, usando como base apenas o artigo original e realizando pesquisas bibliográficas autonomamente, quando necessário. No total, Gauss gerou 200 mil linhas de código Lean (a MathLib, repositório mundial de Lean, alcança cerca de 2 milhões de linhas atualmente), contendo muitos outros resultados relevantes.

O que acontece a seguir?

Comecei a escrever sobre este tema menos de dois meses atrás e nesse período já muita coisa aconteceu. Artigo da revista New Scientist do final de março conta como a formalização em Lean revelou um erro grave num artigo de física, relativo à partícula de Higgs.

Guilherme Silveira, empresário brasileiro com formação em matemática me comunicou como usou automação com IA para obter resultados de pesquisa na área da minha tese de doutorado. Regularmente, os colegas me relatam como a assistência da inteligência artificial está mudando o modo como fazem matemática, e eu vejo o mesmo acontecendo comigo e com meus alunos. Gostemos ou não, a IA chegou para ficar e a matemática nunca mais será a mesma.

LINK PRESENTE: Gostou deste texto? Assinante pode liberar sete acessos gratuitos de qualquer link por dia. Basta clicar no F azul abaixo.