Solucionan problema de esferas: hito en matemáticas

Un equipo de matemáticos, liderado por Maryna Viazovska (galardonada con la Medalla Fields en 2022), ha formalizado la solución al problema del empaquetamiento de esferas en dimensiones 8 y 24, un hito en la verificación matemática. El problema, que se remonta a la conjetura de Kepler en 1611, busca determinar la forma más densa de empaquetar esferas idénticas en un espacio n-dimensional. La formalización, realizada con la ayuda de la herramienta de autoformalización Gauss, ha acelerado significativamente el proceso, reduciendo lo que se estimaba que tomaría seis meses a solo cinco días para la dimensión 8 y dos semanas para la dimensión 24. Este logro, que implica una intrincada combinación de geometría discreta, análisis armónico y teoría de números, ha generado una formalización de aproximadamente 200,000 líneas de código, superando la escala de muchos proyectos de formalización anteriores. La formalización no solo valida un resultado matemático importante, sino que también abre la puerta a una investigación más rápida y a una mejor comprensión de las conexiones entre diferentes áreas de las matemáticas, y plantea desafíos sobre cómo integrar y mantener el conocimiento formal a gran escala en la era de la IA. El proyecto ha sido apoyado por DARPA y cuenta con la colaboración de diversos expertos de la comunidad matemática y de la herramienta Lean.