A marinha brit\u00e2nica abriu a discuss\u00e3o sobre como dispor balas de canh\u00e3o no por\u00e3o de navios para armazenar o maior n\u00famero poss\u00edvel. Esse problema levou ao estudo do empacotamento de esferas, formulado por Johannes Kepler em 1611. A quest\u00e3o central \u00e9 encontrar o arranjo de bolas id\u00eanticas que maximize o aproveitamento do volume.<\/p>\n
Com o tempo, o problema ganhou escala e complexidade. Em 1953, L\u00e1szl\u00f3 T\u00f3th reduziu o desafio a um n\u00famero finito de c\u00e1lculos. Em 1998, Thomas Hales anunciou a conclus\u00e3o desses c\u00e1lculos, mas o texto era extenso demais para revis\u00e3o pr\u00e1tica. O impasse motivou um novo ciclo metodol\u00f3gico.<\/p>\n
Para resolver a prova, Hales iniciou o projeto Flyspeck, transcrevendo cada passo para uma linguagem formal. O objetivo era permitir a verifica\u00e7\u00e3o computacional rigorosa. O esfor\u00e7o durou mais de uma d\u00e9cada e foi conclu\u00eddo em 2014, consolidando a solu\u00e7\u00e3o do empacotamento de esferas em dimens\u00e3o 3.<\/p>\n
Em dimens\u00f5es altas, novas conquistas surgiram. Em 2016, Maryna Viazovska resolveu o caso da dimens\u00e3o 8 e, em seguida, ampliou a solu\u00e7\u00e3o para a dimens\u00e3o 24. Essas realiza\u00e7\u00f5es combinaram teoria dos n\u00fameros, geometria discreta e an\u00e1lise harm\u00f4nica, rendendo reconhecimento internacional e uma Medalha Fields em 2022.<\/p>\n
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\u00e1veis por computador. Gauss, IA especializada em formaliza\u00e7\u00e3o autom\u00e1tica, integrou a equipe da empresa.<\/p>\n
Gauss transformou o teorema de Viazovska em Lean em cinco dias para a dimens\u00e3o 8. Em cerca de duas semanas, adaptou a abordagem \u00e0 dimens\u00e3o 24, baseando-se no artigo original e em pesquisas bibliogr\u00e1ficas quando necess\u00e1rio. O projeto resultou em 200 mil linhas de c\u00f3digo Lean, ampliando o acervo da MathLib.<\/p>\n
A cada nova atualiza\u00e7\u00e3o, surgem desdobramentos no uso de IA para valida\u00e7\u00e3o de teoremas. Um artigo recente sobre falhas em publica\u00e7\u00f5es de f\u00edsica ilustra o potencial da formaliza\u00e7\u00e3o para detectar inconsist\u00eancias. A IA, segundo relatos, j\u00e1 modifica a forma como pesquisadores conduzem e validam trabalhos de matem\u00e1tica.<\/p>\n","protected":false},"excerpt":{"rendered":"