AI ayudó a verificar formalmente por primera vez las demostraciones de una ganadora de la Medalla Fields

En la matemática existe un tipo especial de reconocimiento que está por encima de cualquier premio: cuando una computadora confirma que tu demostración es absolutamente impecable. Las demostraciones de la matemática ucraniana Marina Viazovska, que le valieron la Medalla Fields en 2022, acaban de pasar exactamente por tal verificación — y lo hicieron con participación sin precedentes de la inteligencia artificial.

Viazovska recibió su medalla por resolver uno de los problemas más elegantes y traicioneros de la matemática — el problema del empaquetamiento de esferas. Suena simple: ¿cómo colocas bolas idénticas en el espacio de la manera más densa posible? En dos dimensiones, todo apicultor conoce la respuesta — panales de miel.

En tres dimensiones, una pirámide de esferas es óptima, familiar para cualquiera que haya visto una pila de naranjas en un estante. Pero conforme aumenta el número de dimensiones, el problema se vuelve extraordinariamente complejo. En 2016, Viazovska demostró que la estructura simétrica E8 es el empaquetamiento óptimo en el espacio ocho-dimensional, y poco después, junto con colegas, estableció que la red de Leech es óptima en 24 dimensiones.

A pesar de su aparente abstracción, estos resultados tienen relevancia directa para códigos correctores de errores utilizados por teléfonos inteligentes y sondas espaciales.

La comunidad matemática verificó y reconoció las demostraciones como correctas — de ahí la Medalla Fields. Sin embargo, la verificación formal — un proceso en el cual cada paso lógico de la demostración es verificado por un programa de computadora — es una tarea de escala fundamentalmente diferente. Un revisor humano puede pasar por alto un error sutil, una computadora no puede. Es por eso que la formalización de demostraciones complejas se considera el "estándar de oro" de certeza en la matemática moderna.

Todo comenzó con un encuentro casual. En Lausana, un estudiante de tercer año, Siddharth Hariharan, le contó a Viazovska cómo utilizaba la formalización de demostraciones en el lenguaje Lean para una comprensión más profunda de conceptos matemáticos. Lean es simultáneamente un lenguaje de programación y el llamado "asistente de demostraciones", permitiendo registrar razonamientos matemáticos en una forma que una computadora puede verificar con corrección absoluta.

Viazovska se interesó, y en marzo de 2024, nació el proyecto Formalising Sphere Packing in Lean. Se unieron a él expertos del Imperial College Londres, Universidad de East Anglia y Universidad de California en Berkeley. El equipo creó un "plano" — un mapa legible para humanos de todos los elementos de la demostración ocho-dimensional, señalando cuáles ya habían sido formalizados y cuáles todavía necesitaban ser traducidos a Lean.

Dos años de trabajo meticuloso — y entonces ocurrió un avance. En octubre de 2025, la startup Math, Inc., que desarrolló el sistema de IA Gauss, se unió al proyecto. Esto no es un modelo de lenguaje ordinario: Gauss es un "agente razonador", capaz de alternar entre razonamiento en lenguaje natural e inferencia matemática completamente formalizada. Esencialmente, es una IA que puede traducir automáticamente demostraciones matemáticas en un lenguaje comprensible para un verificador de computadora. Conectar Gauss aceleró dramáticamente el proceso de formalización, permitiendo la conclusión de lo que de otra manera hubiera requerido aún años de trabajo manual.

El resultado resonó significativamente en la comunidad científica. "Estos nuevos resultados se ven muy y muy impresionantes y ciertamente señalan progreso rápido en esta dirección", señaló Liam Foul, postdoctorado de la Universidad de Princeton y experto en razonamiento de IA, quien no participó en el proyecto. Según él, la verificación formal es una especie de "sello de calidad", una garantía absoluta de que cada paso del razonamiento lógico es correcto.

La importancia de este avance va mucho más allá de una única demostración. Hasta hace poco, la formalización de resultados matemáticos serios era un proceso tan laborioso que solo proyectos aislados se atrevían a emprenderlo. Si sistemas de IA como Gauss pueden acelerar sistemáticamente este trabajo, la matemática obtendrá algo sin precedentes: la capacidad de verificar en masa demostraciones acumuladas durante décadas. Esto no es un reemplazo para matemáticos — Viazovska aún realizó un logro intelectual que las máquinas no pueden replicar. Pero la IA resulta indispensable en la parte más rutinaria y crucial del trabajo — verificar que la intuición brillante no condujo a un error en uno de miles de pasos lógicos.

Estamos presenciando el nacimiento de un nuevo modelo de colaboración: los humanos formulan ideas y construyen demostraciones, mientras que las máquinas garantizan su impecabilidad. Para la matemática, donde un error pasado por alto puede poner en duda décadas de investigación subsecuente, esto no es meramente conveniente — es un cambio de paradigma.