Formalizando el Último Teorema de Fermat

Artículo original ↗ Discusión en Hacker News ↗

Un sistema de IA ha producido una formalización completa en Lean del Último Teorema de Fermat en 11 días, generando 13 millones de líneas de código de prueba verificado por máquina para uno de los resultados más famosos de las matemáticas modernas. Los comentaristas ven esto como un hito para la demostración automática de teoremas y los métodos formales, pero plantean preocupaciones sobre la confianza en la verificación (posibles errores en los asistentes de prueba), la legibilidad de las demostraciones y si unas formalizaciones gigantes generadas por IA son reutilizables o significativas para los humanos. El hilo también explora implicaciones más amplias: el coste y la eficiencia del razonamiento a gran escala con IA, su impacto en las carreras matemáticas y la financiación de la investigación, y si los futuros sistemas podrían pasar de formalizar demostraciones conocidas a descubrir otras fundamentalmente nuevas.

Naturaleza del resultado

  • El hilo enfatiza que esto no es una nueva demostración matemática del Último Teorema de Fermat (FLT), sino una formalización en Lean de una demostración existente de estilo Wiles/Taylor.
  • Varios comentaristas señalan que la comunidad matemática ya consideraba el FLT esencialmente resuelto; la novedad está en la escala y la rapidez de la autoformalización.
  • La formalización sigue una exposición de los años 90, no los enfoques más modernos y simplificados, y maneja primos ≥17; otras formalizaciones previas cubren los casos restantes.

Escala, coste y herramientas

  • Claude produjo ~13M líneas de Lean y ~29.5k lemas en ~11 días, usando ~6B tokens de salida y mucho cómputo (cientos de GB de RAM, muchos núcleos).
  • Las estimaciones de coste público están en el orden de cientos de miles de dólares, pero hay debate sobre si la inferencia interna es mucho más barata y cómo amortizar el coste de entrenamiento.
  • Una plataforma colaborativa de Lean (prove2.me) y una orquestación personalizada (“enjambre de agentes”) fueron clave; algunos ven esto como evidencia de que las herramientas estructuradas son cruciales para trabajo serio.

Confianza, corrección y el kernel de Lean

  • Muchos preguntan: ¿cómo se pueden confiar 13M líneas? La respuesta: el verificador de tipos de Lean comprueba cada paso; los humanos principalmente necesitan confiar en:
    • la formulación formal del FLT,
    • el kernel pequeño y los axiomas,
    • y un comprobador secundario (“comparador”) que re-verifica el teorema final.
  • Otros advierten que Lean ha tenido errores recientes de solidez, incluyendo una “refutación” de Collatz hallada por IA que explotaba un fallo del kernel; múltiples comprobadores independientes reducen, pero no eliminan, el riesgo.
  • Algunos quieren traducción a otros sistemas (p. ej., HOL/Metamath) para mayor garantía.

Valor para las matemáticas y reutilización

  • Los partidarios: los enormes esfuerzos de demostración suelen generar muchas abstracciones reutilizables; la autoformalización puede detectar errores en la literatura y reducir la carga de los revisores.
  • Los escépticos: 13M líneas pueden ser “AI slop” con abstracciones pobres, difíciles de integrar en bibliotecas estándar; quizá no avance la comprensión humana.
  • Un proyecto humano en curso de formalización del FLT tenía objetivos distintos: aportar componentes limpios y generales de mathlib y un “documento dinámico” explorable por humanos.

Impacto en matemáticos y carreras

  • Emociones mezcladas: asombro por la capacidad, preocupación por investigadores en etapas iniciales que sean “adelantados” por LLMs.
  • Algunos argumentan que formalizar es distinto de descubrir demostraciones, así que sigue habiendo un gran papel para la creatividad y la exposición humanas.

Implicaciones éticas y de IA más amplias

  • Los optimistas ven esto como evidencia de que la IA puede abordar grandes porciones de las matemáticas y, por analogía, problemas científicos (p. ej., medicina, física).
  • Los pesimistas se preocupan por la concentración de poder, los presupuestos opacos de cómputo, el bombo para IPOs y el acceso limitado del público a los modelos más potentes.
  • Aparece un debate filosófico sobre el sentido humano, “hacerse dios” (p. ej., curar el envejecimiento) y si el progreso de la IA mejora o socava el bienestar humano.

Direcciones futuras

  • Próximos objetivos sugeridos: la clasificación de los grupos simples finitos, la Hipótesis de Riemann, P vs NP.
  • Varios quieren que pasadas posteriores de IA simplifiquen y refactoricen radicalmente la formalización del FLT, o demuestren que es casi mínima en algún sentido formal.