La IA ayuda por primera vez a verificar formalmente las demostraciones de una ganadora de la Medalla Fields

En matemáticas existe un tipo de reconocimiento que está por encima de cualquier premio: que un ordenador confirme 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 superar justo esa prueba, con una participación sin precedentes de la inteligencia artificial.

Viazovska obtuvo su medalla por resolver uno de los problemas más elegantes y traicioneros de las matemáticas: el empaquetamiento de esferas. Suena sencillo: ¿cómo colocar bolas idénticas en el espacio de la forma más densa posible? En dos dimensiones, cualquier apicultor conoce la respuesta: el panal.

En tres dimensiones, lo óptimo es la pirámide de bolas que conoce cualquiera que haya visto una pila de naranjas en un puesto del mercado. Pero a medida que crece el número de dimensiones, el problema se vuelve monstruosamente difícil. En 2016, Viazovska demostró que la estructura simétrica E8 es el mejor empaquetamiento en el espacio de ocho dimensiones y, poco después, junto con otros colegas, estableció que la red de Leech es óptima en 24 dimensiones.

Por abstractos que parezcan, estos resultados tienen relación directa con los códigos de corrección de errores que usan los teléfonos inteligentes y las sondas espaciales.

La comunidad matemática revisó las demostraciones y las dio por correctas; de ahí la Medalla Fields. Sin embargo, la verificación formal, un proceso en el que un programa informático comprueba cada paso lógico de la demostración, es una tarea de una escala radicalmente distinta. Un revisor humano puede pasar por alto un error sutil; un ordenador, no. Por eso la formalización de demostraciones complejas se considera el "estándar de oro" de la fiabilidad en la matemática actual.

Todo empezó con un encuentro casual. En Lausana, Sidharth Hariharan, estudiante de tercer curso, le contó a Viazovska cómo usaba la formalización de demostraciones en el lenguaje Lean para comprender a fondo los conceptos matemáticos. Lean es a la vez un lenguaje de programación y un llamado "asistente de demostraciones", que permite escribir razonamientos matemáticos en una forma que el ordenador puede comprobar con absoluta corrección.

Viazovska se interesó y en marzo de 2024 nació el proyecto Formalising Sphere Packing in Lean. Se sumaron expertos del Imperial College de Londres, la Universidad de East Anglia y la Universidad de California en Berkeley. El equipo elaboró un "plano" (blueprint): un mapa legible para humanos de todos los elementos de la demostración en ocho dimensiones, que indicaba cuáles ya estaban formalizados y cuáles quedaban por traducir a Lean.

Siguieron dos años de trabajo minucioso y después llegó el punto de inflexión. En octubre de 2025 se incorporó al proyecto la startup Math, Inc., creadora del sistema de IA Gauss. No es un modelo de lenguaje corriente: Gauss es un "agente de razonamiento" capaz de alternar el razonamiento en lenguaje natural con una deducción matemática totalmente formalizada. En la práctica, es una IA capaz de traducir automáticamente demostraciones matemáticas a un lenguaje que entiende un verificador informático. Gauss aceleró radicalmente la formalización y permitió terminar lo que de otro modo habría requerido años más de trabajo manual.

El resultado tuvo una fuerte repercusión en la comunidad científica. "Estos nuevos resultados parecen muy, muy impresionantes y sin duda señalan un progreso rápido en esta dirección", afirmó Liam Fowl, investigador posdoctoral de la Universidad de Princeton y experto en razonamiento de IA, que 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 sola demostración. Hasta hace poco, formalizar resultados matemáticos de peso era tan laborioso que solo se embarcaban en ello proyectos aislados. Si sistemas de IA como Gauss logran acelerar este trabajo de forma sistemática, la matemática ganará algo sin precedentes: la posibilidad de verificar en masa demostraciones acumuladas durante décadas. Esto no sustituye a los matemáticos: Viazovska siguió logrando una hazaña intelectual que una máquina no puede repetir. Pero la IA resulta insustituible en la parte más rutinaria y delicada del trabajo: comprobar que la intuición genial no condujo a un error en alguno de los miles de pasos lógicos.

Estamos viendo nacer un nuevo modelo de colaboración: el humano formula ideas y construye demostraciones, y la máquina garantiza que son impecables. Para una disciplina en la que un solo error inadvertido puede poner en duda décadas de investigación posterior, esto es más que una comodidad: cambia la forma de trabajar de la disciplina.