Investigadores se reunieron esta semana en Londres para acelerar la formalización del último teorema de Fermat mediante modelos avanzados de IA. El taller se centra en convertir la demostración de 1993 de Andrew Wiles en código Lean para su verificación informática. El progreso ha sido rápido, duplicándose las líneas de código tras el primer día.
Veinticinco matemáticos, científicos informáticos y expertos en IA se reunieron en un hotel del centro de Londres para trabajar en el proyecto dirigido por Kevin Buzzard, del Imperial College London. El esfuerzo, con una duración prevista de cinco años y financiado en 2024, tiene como objetivo añadir el teorema al repositorio Mathlib de matemáticas formalizadas. Antes del taller, el proyecto contaba con 20.000 líneas de código. Tras el primer día, el total alcanzó las 40.000. Buzzard señaló que las capacidades de la IA han mejorado notablemente desde diciembre del año pasado, lo que permite al equipo abordar una mayor parte de las matemáticas subyacentes de lo previsto originalmente. Hang Lu Su, también del Imperial College London, describió el proceso como una industrialización del trabajo intelectual. Los participantes están utilizando modelos como Claude para generar y refinar código, aunque persisten preocupaciones sobre la verbosidad y la capacidad de mantenimiento a largo plazo de los resultados producidos por la IA. Buzzard expresó su confianza en que los objetivos originales se cumplirán al finalizar el proyecto. El avance del equipo en la pirámide completa de teoremas de apoyo dependerá de futuros desarrollos en IA.