Con 13 millones de líneas de código en 11 días, Claude formula el último teorema de Fermat

La empresa "Anthropic" anunció que el modelo de inteligencia artificial "Claude" logró, de forma casi independiente, formular el "último teorema de Fermat" en forma de código informático en tan solo 11 días.

Como resultado, se generaron aproximadamente 13 millones de líneas de código en el lenguaje "Lean", y alrededor de 29.500 teoremas intermedios, lo que equivale a unas cinco veces el tamaño de toda la biblioteca matemática formal "Mathlib".

Se recuerda que el matemático francés Pierre de Fermat formuló el teorema en el siglo XVII, pero su demostración permaneció inaccesible durante más de tres siglos, hasta que el matemático británico Andrew Wiles logró probarlo en 1995, tras trabajar en él en secreto durante casi siete años.

La formulación formal significa traducir la prueba matemática a código informático, permitiendo que la computadora verifique la validez de cada paso.

Varios matemáticos intentaron encontrar una prueba para este problema, pero sus esfuerzos terminaron en fracaso. Wiles trabajó en el problema en secreto durante siete años antes de anunciar un gran avance en 1993. Las pruebas matemáticas generalmente consisten en largas cadenas de razonamientos lógicos que dependen unos de otros, de modo que si un error se introduce en alguna etapa, puede hacer colapsar toda la prueba.

Esto fue exactamente lo que ocurrió con Wiles, cuando se descubrió una brecha en su prueba, y le tomó aproximadamente un año corregirla.

La digitalización o formalización de las teorías matemáticas permite trasladarlas del mundo del "papel y lápiz" al mundo del código informático, permitiendo que las computadoras procesen y verifiquen paso a paso la lógica, detectando errores o vulnerabilidades. El repositorio central "Mathlib" contiene aproximadamente dos millones de líneas de matemáticas formalizadas.

El profesor Kevin Buzzard, de Imperial College London, tardó cinco años en llevar a cabo esta tarea, mientras que el modelo "Claude" lo completó en solo 11 días. Según Buzzard, la prueba "no depende de nada más que de los axiomas de las matemáticas".

La tarea se dividió entre agentes de inteligencia artificial que recibían instrucciones generales periódicamente, y les ayudaron a coordinar el trabajo herramientas como "Prove2Me", diseñada originalmente para asistir a matemáticos humanos.

Si estos resultados son reproducibles de manera confiable, el inteligencia artificial podría acelerar el proceso de traducción de las matemáticas modernas a formas verificables automáticamente.