Momento Decisivo para la Colaboración Humano-IA en Matemáticas
La verificación formal asistida por IA de las pruebas de empaquetamiento de esferas de Maryna Viazovska marca un progreso significativo en la colaboración investigativa matemática.Resumen
El trabajo ganador de la Medalla Fields de la matemática ucraniana Maryna Viazovska sobre el empaquetamiento óptimo de esferas en múltiples dimensiones ha sido formalmente verificado mediante una colaboración entre humanos e IA, señalando un progreso rápido en la asistencia de la IA a la investigación matemática.
La investigación original de Viazovska resolvió el problema del empaquetamiento de esferas para 8 dimensiones (usando el arreglo E8) y 24 dimensiones (usando la red Leech), lo cual ya fue verificado por la comunidad matemática. Sin embargo, la verificación formal—la capacidad de un programa para ser verificado por una computadora usando un asistente de pruebas como Lean—es un desafío distinto. Este proyecto, "Formalising Sphere Packing in Lean," comenzó después de que Sidharth Hariharan se conectara con Viazovska para formalizar sus pruebas.
La colaboración se aceleró cuando Math, Inc., utilizando su agente de razonamiento IA llamado Gauss, contribuyó con formalizaciones automáticas. Gauss primero probó 30 hechos intermedios para el caso de 8 dimensiones. Posteriormente, una versión mejorada de Gauss autoformalizó toda la prueba de 8 dimensiones en cinco días, incluso encontrando y corrigiendo un error tipográfico en el artículo publicado. Luego, Gauss autoformalizó la prueba de 24 dimensiones, mucho más compleja, en solo dos semanas. Tanto los colaboradores humanos como los desarrolladores de IA ven esto como un logro colaborativo revolucionario, sugiriendo que esta tecnología liberará a los matemáticos para que se concentren en el descubrimiento conceptual.
(Fuente：ieeespectrum)