La IA verifica uno de los teoremas más complejos de la historia y eso significa que las matemáticas podrían no volver a ser las mismas

• Retan a una IA a diseñar vida desde cero y el resultado es un espécimen que desafía a la biología
• Desafían a ChatGPT a resolver un problema físico 'imposible' y encuentra el patrón oculto en menos de 12 horas

La inteligencia artificial acaba de protagonizar un avance que podría marcar un antes y un después en la historia de las matemáticas. Un sistema de IA ha logrado verificar formalmente una de las demostraciones más complejas de los últimos años, vinculada al célebre problema del empaquetamiento de esferas, un resultado premiado con la prestigiosa Medalla Fields.

El logro se relaciona con el trabajo de la matemática ucraniana Maryna Viazovska, quien en 2022 resolvió el problema del empaquetamiento de esferas en 8 y 24 dimensiones, dos casos que durante décadas habían resistido los intentos de los investigadores y que le valió la Medalla Fields. Ahora, una colaboración entre matemáticos y inteligencia artificial ha conseguido traducir esas complejas demostraciones a un formato verificable por ordenador.

De ello ha hablado Kit Yates, profesor de biología matemática, en un extenso artículo publicado en Live Science. En él se explica cómo la verificación automática de pruebas matemáticas podría abrir una nueva etapa en la forma de construir y validar conocimiento dentro de esta disciplina.

Una prueba matemática extremadamente compleja

El problema del empaquetamiento de esferas intenta responder a una cuestión aparentemente simple: cómo colocar esferas idénticas en un espacio para que ocupen el mayor volumen posible sin superponerse. Aunque resulta intuitivo en tres dimensiones, la dificultad aumenta de forma radical cuando se analiza en espacios de mayor dimensión.

Durante décadas, el problema solo se había resuelto completamente en una, dos y tres dimensiones. Las soluciones halladas por Viazovska para los casos de 8 y 24 dimensiones fueron consideradas un logro extraordinario dentro de la matemática moderna y le valieron el reconocimiento de la comunidad científica internacional.

El papel de la inteligencia artificial

El paso decisivo ahora ha consistido en transformar esas demostraciones en código matemático formal capaz de ser comprobado por ordenador. Para ello se utilizó Lean, un sistema de verificación que exige describir cada definición y cada inferencia lógica con total precisión para que una máquina pueda validar todos los pasos del razonamiento.

El proceso contó además con la ayuda de Gauss, un agente de razonamiento desarrollado por la empresa Math, Inc. Este sistema de inteligencia artificial ayudó a convertir las demostraciones humanas en pruebas verificables por Lean, acelerando tareas que tradicionalmente podían requerir meses o incluso años de trabajo especializado.

TE PUEDE INTERESAR

Retan a una IA a resolver cuatro problemas matemáticos 'imposibles' y lo que sucede dice mucho del futuro que nos aguarda

R. Badillo

Gracias a esta colaboración entre humanos y máquinas, el sistema completó en pocos días el trabajo que los propios matemáticos estimaban que habría requerido meses de revisión manual. El resultado es una demostración verificada paso a paso con un nivel de precisión difícil de alcanzar incluso para grandes equipos de expertos.

Para muchos especialistas, este avance apunta a un cambio profundo en la forma de hacer matemáticas. Las herramientas de inteligencia artificial podrían encargarse de revisar miles de detalles técnicos, permitiendo que los investigadores concentren su esfuerzo en la intuición, la estrategia y las ideas que impulsan nuevos descubrimientos.