Hoy se ha publicado el anuncio de la formalización total de los teoremas de Maryna Viazovska sobre el empaquetamiento de esferas. Con una extensión de aproximadamente 200,000 líneas de código en el lenguaje Lean, este proyecto se consagra como la mayor formalización de propósito único en la historia y el primer resultado galardonado con la Medalla Fields de este siglo en ser verificado íntegramente por computadora.

El núcleo matemático de este logro reside en resolver el milenario problema del empaquetamiento de esferas: ¿cómo disponer esferas idénticas en un espacio n-dimensional de la forma más densa posible? Mientras que para tres dimensiones la solución (conjeturada por Kepler en 1611) requirió siglos de esfuerzo y una compleja verificación computacional, Viazovska halló una solución "sorprendentemente simple" para la dimensión 8 mediante el uso de formas modulares. Su trabajo, extendido posteriormente a la dimensión 24 junto a otros colaboradores, demuestra que la red \(E_8\) y la red de Leech son los arreglos más densos y óptimos en sus respectivas dimensiones. La prueba es célebre por tender un puente magistral entre la geometría discreta, el análisis armónico y la teoría de números.

Una pieza clave de este éxito ha sido Gauss, un sistema de inteligencia artificial que ha transformado radicalmente los tiempos de ejecución. Mientras que proyectos de envergadura similar solían requerir décadas de esfuerzo humano, Gauss logró completar tareas críticas en cuestión de semanas. De manera sorprendente, la IA no solo finalizó la demostración en la dimensión 8 en apenas cinco días —un trabajo estimado en seis meses para un equipo humano—, sino que abordó la dimensión 24 de forma autónoma, realizando búsquedas bibliográficas y optimizando el código generado hasta reducirlo de medio millón de líneas a una versión más eficiente y mantenible.

Este avance trasciende la mera verificación; representa un cambio de paradigma en la investigación científica. Al convertir teorías complejas en datos navegables, modulares y procesables por máquinas, se abre la puerta a una nueva era de colaboración humano-IA. El éxito del proyecto demuestra que la autoformalización no solo es posible, sino que es capaz de integrar ramas diversas de la matemática en un corpus de conocimiento unificado y verificable a escala global.

Para conocer todos los pormenores técnicos y el alcance de este logro, se pueden consultar los detalles en: Completing the formal proof of higher-dimensional sphere packing.