Em coluna na Folha, Viana fala sobre o futuro da matemática após IA
Reprodução da coluna de Marcelo Viana na Folha.
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.