Claude demuestra el último teorema de Fermat en 11 días

>La velocidad con la que pudimos producir esta prueba demuestra que ahora es posible formalizar grandes extensiones de las matemáticas, lo que puede tanto detectar errores en el cuerpo común de las pruebas matemáticas como reducir la carga de revisar nuevos trabajos.

^ esta sección debería haber estado en los primeros párrafos, en mi opinión. Explicar por qué esto es relevante no debería estar tan abajo.

"La prueba no es la prueba moderna que yo mismo he estado formalizando siguiendo ideas de Khare, Taylor, etc., sino la exposición de Darmon–Diamond–Taylor de 1995 del argumento de Wiles–Taylor–Wiles, a través del teorema de Langlands–Tunnell y el teorema de reducción de nivel de Ribet. El repositorio de Anthropic desarrolla la teoría de Fontaine (para estudiar deformaciones planas de representaciones de Galois) y desarrolla suficiente del trabajo de Mazur sobre el ideal de Eisenstein para concluir que ninguna curva de Frey puede tener un punto de orden p>=17. Esto significa que su prueba de FLT solo funciona para p>=17, sin embargo, FLT ya estaba formalizado para primos regulares impares por Best-Birkbeck-Brasca-Rodriguez, y el primo irregular más pequeño es 37, así que todo está bien."

Mi pregunta para cualquier matemático que lea esto: ¿lo anterior tiene algún sentido para ustedes?

Lo pregunto porque puedo leer la mayoría del material técnico relacionado con ingeniería informática, programación, especificaciones de hardware, etc. Incluso si no entiendo completamente todos los detalles, puedo seguirlos bastante bien. Así que me pregunto si los matemáticos profesionales pueden mirar lo anterior y aún darle sentido, como los ingenieros de software experimentados lo hacen con cosas de computación.

> En el proceso, escribió 13 millones de líneas de Lean y demostró 29,500 teoremas intermedios.

Bastante increíble. Supongo que da más crédito a la idea de que cualquier cosa que se pueda demostrar que es correcta puede ser hecha por un modelo.

> un equipo de agentes completó la prueba en poco menos de dos semanas, consumiendo alrededor de seis mil millones de tokens de salida de un modelo de investigación interno de propósito general, aproximadamente comparable a Claude Fable 5.1.

A $50/M tokens de salida, esto habría costado del orden de $300k (más un poco por tokens de entrada/prefill) a las tarifas de API.

En una nota tangencial, recomiendo encarecidamente este libro de Simon Singh.

https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)

13M de líneas de código, ¿estamos seguros de que no explotó ningún problema latente en el sistema de pruebas de Lean?

Veremos cada vez más anuncios de este tipo a medida que las herramientas de IA escalen. Por impresionante que sea la codificación agéntica, palidece en comparación con la propuesta de valor de la investigación médica, matemática y física.

Espero optimistamente ser testigo del advenimiento de una 'panacea' global en mi vida gracias a los esfuerzos de la IA. Ingeniería genética a gran escala rentable, una cura para cada enfermedad, potencialmente incluso una cura para el envejecimiento.

El futuro es a la vez hermoso y aterrador.

Con lo capaz y barato que se está volviendo la verificación automática de pruebas, me pregunto cuántas pruebas que se suponen verdaderas por casi toda la comunidad matemática resultarán ser falsas. Y no por algún error marginal fácil de corregir, sino por algún defecto fundamental en el razonamiento.

¡Ok, consigamos una jauría rabiosa de agentes trabajando en P = NP? a continuación!