Avances en la formalización del último teorema de Fermat
(xenaproject.wordpress.com)- El trabajo de trasladar la demostración de FLT a Lean lleva dos meses en marcha, y aunque las definiciones de R y T necesarias para el teorema “R=T” de Wiles aún no están completas, ya se demostró un resultado de álgebra conmutativa abstracta
- El objetivo no es replicar tal cual la demostración original de los años 90, sino construir sobre Lean y mathlib una demostración generalizada y simplificada a partir de trabajos posteriores de Diamond/Fujiwara, Kisin, Taylor, Scholze y otros
- Mientras se formalizaba la cohomología cristalina necesaria para la demostración moderna, salió a la luz un problema: un lema clave del artículo de Roby de 1965, una referencia estándar sobre estructuras de potencias divididas, parece ser incorrecto
- Brian Conrad encontró una demostración alternativa en el apéndice del libro de Berthelot-Ogus, y Arthur Ogus también respondió que sabía cómo corregir errores de ese apéndice, por lo que el proyecto pudo avanzar de nuevo
- Este caso muestra el riesgo de que las demostraciones detalladas de las matemáticas modernas dependan de la memoria de especialistas y conocimiento tácito, y refuerza las razones prácticas para registrar demostraciones en sistemas formales
Estado actual de trasladar la demostración de FLT a Lean
- El trabajo de enseñarle a una computadora la demostración del último teorema de Fermat (FLT) lleva dos meses en marcha
- Definir en Lean qué son R y T en el teorema “R=T”, pieza central de la demostración de Wiles, requiere mucho trabajo, y ninguna de las dos definiciones está terminada todavía
- El estudiante de doctorado Andrew Yang ya demostró el resultado necesario de álgebra conmutativa abstracta
- Es un resultado de la forma “si unos anillos abstractos R y T satisfacen varias condiciones técnicas, entonces son iguales”
- El borrador actual está publicado como blueprint
- Los sistemas usados son Lean y la biblioteca matemática mathlib
- Quienes sepan un poco de Lean y teoría de números pueden participar a través de las guías de contribución, el panel del proyecto y los issues
Por qué no se está trasladando tal cual la demostración de los años 90
- El proyecto no formaliza tal cual la demostración de Wiles de los años 90
- Trabajos posteriores de Diamond/Fujiwara, Kisin, Taylor, Scholze y otros hicieron que la demostración fuera más general y más simple
- El objetivo no es solo demostrar FLT, sino también construir dentro de Lean resultados más generales y potentes
- Si la revolución de la IA en matemáticas realmente ocurre y Lean se convierte en un componente importante, puede ser útil que las computadoras tengan las definiciones centrales de la teoría de números moderna en una forma que puedan entender
Potencias divididas necesarias para la cohomología cristalina
- La demostración que se busca formalizar usa cohomología cristalina, que no aparecía en la demostración original de Wiles
- Esta teoría se desarrolló en París en las décadas de 1960 y 1970, y Berthelot sentó sus bases a partir de ideas de Grothendieck
- Las funciones exponencial y logarítmica clásicas son importantes para entender la geometría diferencial y la cohomología de de Rham, pero en contextos aritméticos como característica p no funcionan de la misma manera
- Las estructuras de potencias divididas, desarrolladas en los artículos de Roby de los años 60, cumplen un papel central para construir funciones análogas utilizables en contextos aritméticos
- Para enseñarle cohomología cristalina a Lean, primero hay que formalizar las potencias divididas
El problema en la literatura de Roby que apareció durante el trabajo en Lean
- Antoine Chambert-Loir y Maria Ines de Frutos Fernandez estaban formalizando en Lean la teoría de potencias divididas
- Durante el verano, Lean reveló un problema en un argumento humano de la literatura estándar, y al revisarlo parecía que un lema clave del trabajo de Roby era incorrecto
- Técnicamente, el artículo de Berthelot no desarrolla la teoría de potencias divididas desde cero, sino que usa “Les algebres a puissances divisees” de Roby
- Ese artículo fue publicado en Bull Sci Math, 2ième série, 89, 1965, pp. 75-91
- El Lemme 8 de la p. 86 parece ser falso, y no estaba claro cómo corregir su demostración
- Esa demostración cita incorrectamente otro lema del artículo de Roby de 1963 en Ann Sci ENS
- La proposición correcta es
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R), pero en la aplicación faltaba un producto tensorial
- Este problema rompe la demostración de Roby de que el álgebra de potencias divididas de un módulo tiene potencias divididas, y como resultado impedía definir el anillo
A_cris
Una situación más cercana a “falta una demostración” que a “la teoría está equivocada”
- Esto no significa que la cohomología cristalina en sí esté sustancialmente equivocada
- Los teoremas principales aún parecen ser correctos, pero la demostración que seguían Antoine y Maria Ines era incompleta
- Roby, Grothendieck y Berthelot ya fallecieron, así que no era posible preguntarles directamente a los expertos originales
- Varios especialistas consideran que, aunque un lema intermedio sea falso, la demostración del resultado principal se puede corregir
- En una formalización no basta con juzgar que “debería poder corregirse”: se necesita una demostración realmente corregida
El rodeo que abrió el apéndice de Berthelot-Ogus
- Tadashi Tokieda contó esta historia en Stanford a Brian Conrad, y Conrad preguntó de qué se trataba eso de que la cohomología cristalina estaba mal
- Tras escuchar los detalles técnicos, Conrad estuvo de acuerdo en que parecía haber un problema y se puso a revisarlo
- Unas horas después, Conrad informó que en el apéndice del libro de Berthelot-Ogus sobre cohomología cristalina había otra demostración de que el álgebra universal de potencias divididas de un módulo tiene potencias divididas
- Desde el punto de vista de Conrad, ese enfoque parecía válido, y gracias a eso la demostración pudo seguir avanzando
- Más tarde, durante un almuerzo con Arthur Ogus en Berkeley, al contarle que ese apéndice había resuelto el problema, Ogus respondió que ese apéndice también tenía varios errores, pero que sabía cómo corregirlos
Por qué la literatura matemática moderna necesita formalización
- Este proceso muestra que la forma en que los humanos documentan las matemáticas modernas puede no ser lo bastante robusta
- Muchos hechos quedan como “cosas que los expertos saben” y pueden no estar ordenados con precisión en la literatura
- Aunque las ideas importantes sean lo bastante sólidas como para resistir este tipo de sobresaltos, las demostraciones detalladas reales pueden no estar donde se esperaba
- Registrar correctamente las matemáticas en sistemas formales puede reducir mucho la posibilidad de errores
- Incluso para matemáticos que no son formalistas, si se quiere que las máquinas aprendan los argumentos humanos y lleguen a hacer matemáticas por sí mismas, primero hace falta enseñarles esos argumentos a las máquinas
- Maria Ines dio una charla sobre la formalización de potencias divididas en el Cambridge Formalization of Mathematics seminar, y se entiende que esos problemas ya fueron resueltos
- El proyecto volvió a encaminarse, aunque sigue existiendo la posibilidad de que la literatura vuelva a poner obstáculos
1 comentarios
Comentarios en Hacker News
Me recordó cuando en el posgrado escribía código rápido para ayudar con el enfoque computacional de mi asesor sobre la conjetura de Birch–Swinnerton-Dyer
En un seminario de teoría de números en una ciudad cercana, me preguntaron si estaba tratando de reforzar la evidencia a favor de la conjetura y respondí entre risas: “No, más bien quiero encontrar un contraejemplo”, lo que enfureció bastante a los expertos
La teoría de números es tan antigua y profunda que escribir una tesis doctoral en ese campo se siente casi como el primer paso para volverse principiante; aunque conocía la notación y las definiciones, no lograba alcanzar la intuición que hay debajo
Por eso, la indignación que mostraron los expertos ante la idea de “esperar un contraejemplo” me dejó más curiosidad que miedo, y me pregunté qué era lo que ellos veían pero todavía no podían expresar con palabras
Este tipo de avances en la formalización hace que las matemáticas sean mucho más accesibles para quienes están más familiarizados con la programación
La inquietud por la falta de formalidad es válida, pero creo que la reacción correcta ante esa inquietud no es evitarla, sino sentir curiosidad
Si un novato inexperto como tú encontrara un contraejemplo con cálculos rústicos y se hiciera famoso de la noche a la mañana, todo ese esfuerzo y toda esa estructura podrían venirse abajo, así que entiendo que se hayan molestado
Si pudiera darle un consejo sobre el posgrado en matemáticas a mi yo más joven, le diría que dedicara al menos una cuarta parte del tiempo de cada tarea no trivial de “demuestra X” a buscar contraejemplos
En las tareas fallarás el 99% de las veces, pero tu comprensión del problema crecerá muchísimo, y en el 1% restante puedes parecer un genio
Cuando entras a la investigación matemática real, esa probabilidad cambia de forma mucho más favorable hacia un enfoque de priorizar contraejemplos
Recuerdo que cuando era estudiante un amigo me contó que alguien había terminado el primer día de un seminario y todos estaban emocionados diciendo que esa persona iba a demostrar el último teorema de Fermat
Esa persona era Andrew Wiles, y después pasó unos meses corrigiendo un problema detectado antes de la publicación, hasta que por fin se publicó todo
Para quienes estudiábamos matemáticas, fue un acontecimiento tremendamente emocionante, así que cuando veo la expresión “prueba anticuada de los años 90” realmente me hace sentir viejo
Casi toda la clase estaba formada por estudiantes de posgrado en matemáticas y creo que no entendí ni el 20% del material
Me gustó la parte donde dicen que Lean hizo una de esas cosas irritantes que a veces hace: se quejó de cómo la literatura estándar presenta un argumento humano y, al revisarlo con detalle, resultó que efectivamente faltaban partes en el razonamiento humano
Más allá de la molestia en tono de broma, esto es algo impresionante, y creo que Lean y otros demostradores de teoremas van a ser herramientas importantes para las matemáticas en el futuro
La parte sobre lo mala que es la documentación matemática moderna se siente parecida a UI/UX/diseño web
Un diseñador hace maquetas, prototipos y flujos de interacción informales e imprecisos y se los entrega al desarrollador, y el desarrollador tiene que formalizarlos en código y explicárselos con precisión a una máquina
En ese proceso inevitablemente aparecen huecos, como escenarios de interacción o rutas de código que el diseño no había considerado, y a veces salen a la luz defectos graves de diseño que el desarrollador o el diseñador tienen que corregir
Diseño y desarrollo son funciones distintas y exigen formas de pensar diferentes, y la mayoría de los diseñadores muestran una fuerte resistencia a trabajar y pensar como desarrolladores
Después de ese fracaso aprendimos que no podemos formalizar por completo las matemáticas, y eso apunta al problema fundamental de los enfoques que intentan hacer matemáticas con IA
Si te interesa este tema, vale la pena ver el código real
Por ejemplo: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
También vale la pena ver el plano general que explica la estructura completa del código: https://imperialcollegelondon.github.io/FLT/blueprint/
Lo veo desde fuera, pero me parece muy interesante observar cómo se ve el código en Lean y cómo contribuye la gente
También me gusta que no haga falta tener pruebas unitarias. En cierto sentido, el enunciado de la demostración final es la prueba unitaria
Por ejemplo, ejemplos triviales y contraejemplos para comprobar que una definición no está vacía cumplen esa función
Desde la perspectiva de alguien que hizo matemáticas puras, el gran problema es que los matemáticos casi nunca proporcionan demostraciones autocontenidas.
No tienen incentivos para hacerlo, y a veces los autores incluso se enorgullecen de “omitir los detalles”.
Al final, si uno quiere una demostración rigurosa en la que pueda seguir todos los pasos lógicos, hace falta que un experto rellene huecos que no se encuentran fácilmente en la literatura.
A veces eso solo se vuelve posible si esa persona escribe un libro explicándolo todo, y en ocasiones ni siquiera eso basta.
Si nos atenemos solo a lo que está registrado, gran parte de la matemática moderna está sobre una base inestable.
Los artículos de investigación matemática se escriben para otros expertos del área, y a veces tienen tan pocos detalles que uno suele quejarse de eso en la revisión por pares.
Pero si realmente se incluyeran todos los detalles, los artículos serían mucho más largos.
Como ejemplo que puede resolverse con una buena base de matemáticas de preparatoria, se puede plantear demostrar que existen constantes C, X > 0 tales que para cualquier número real x > X se cumple
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx.Este tipo de proposiciones aparecen todo el tiempo en teoría analítica de números y, para un experto, son obvias, así que en los artículos casi siempre se escriben sin demostración.
Si se hiciera una demostración completa y rigurosa, sería larga y aburrida, y ningún experto querría leerla.
Esta actitud tiene un costo de compromiso, pero parece mantenerse en un nivel manejable.
Suena como la tercera etapa que menciona Tao: intuición informada.
Decía: “Si ya has hecho algo 100 veces, puedes decir ‘como se observa fácilmente’ y seguir adelante”.
Entendí que sería como pedirle a una persona con una base de datos mental que encontrara si encajan las precondiciones de cierto teorema y la conclusión de la oración siguiente.
O me pregunto si existe matemática que no puede expresarse de una forma que los verificadores de pruebas actuales puedan evaluar.
También podría ser que el uso de verificadores de pruebas no esté tan difundido como uno pensaría. Suena parecido al lugar que ocupan los lenguajes con tipado estático en programación.
Es decir, quisiera saber si ha habido casos en los que una demostración ampliamente aceptada tuviera un defecto fatal por una parte que se dejó pasar con gestos de mano.
Si eso nunca ha ocurrido, también se entiende por qué existe una actitud relajada respecto a explicitar los detalles.
Siempre me he preguntado si de verdad es correcta esa intuición de que “crystalline cohomology se ha usado tanto desde los años 70 que, si hubiera habido un problema, ya se habría descubierto hace mucho”.
¿De verdad es tan imposible que todo un campo de las matemáticas se desarrolle sobre una demostración defectuosa y que ese campo simplemente termine revelándose como falso?
Él vio de primera mano cómo un campo entero podía derrumbarse por un error en “el primer lema de la primera página” de un artículo fundacional.
El flujo que llevó al trabajo inicial en UniMath, al año especial en el IAS y al libro de HoTT puede verse como lo que empujó el tema de la formalización matemática hasta donde está hoy.
Si los fundamentos estuvieran mal, uno de esos contraejemplos podría refutar hasta el teorema base, así que construir sobre fundamentos incorrectos en realidad aumenta la probabilidad de revelar defectos en esos fundamentos.
De manera parecida, cuando a veces se aplica la matemática para hacer predicciones, si la matemática estuviera mal, las predicciones también lo estarían, y esas predicciones equivocadas atraerían mucha atención.
En realidad, la palabra “campo” es un poco engañosa; muchas teorías se parecen más a un nudo atado con varias otras teorías de toda la matemática.
Y esas teorías, a su vez, están conectadas con otras más.
Sería una situación muy extraña que solo la base se derrumbara lógicamente sin afectar en absoluto a otras partes de ese nudo.
En el ejemplo de cohomología de este artículo, cuesta imaginar una enorme masa flotante de matemáticas, internamente totalmente coherente, pero con un solo error.
En sentido estricto, esto se parece más a una postura filosófica, pero me gustaría creer que gran parte de la matemática actual, en cierto sentido, fue descubierta de manera natural.
Spoiler: aun así, el mundo siguió girando.
Durante aproximadamente el último año he intentado de forma intermitente formalizar en Lean parte de un curso de análisis complejo de licenciatura
He aprendido mucho y también ha sido gratificante, pero a veces resultó frustrante
Recién hace poco pude definir por completo la forma polar como una biyección de C* a (-pi,pi] x R, porque insistí en definirlo “desde cero” a pesar de que los números complejos, las series de potencias,
expysinya existen en mathlibEs muy probable que buena parte de la dificultad haya surgido de que solo tengo una licenciatura en matemáticas, no estoy familiarizado con Lean/mathlib y no tengo a nadie que me guíe. Aun así, la comunidad de Zulip fue de gran ayuda
Muchos resultados de mathlib están enunciados de forma bastante abstracta, así que es difícil ver cómo se conectan con los teoremas estándar de licenciatura o incluso saber si esos teoremas están en mathlib
Eso tiene sentido dentro de la comunidad de matemáticas de investigación, pero personalmente fue un gran obstáculo, y podría convertirse en un problema parecido si Lean se usara más en educación. Aun así, es algo que se puede organizar con el tiempo
Sigo pensando que la automatización de pruebas todavía no es suficiente
Demasiadas cosas son más difíciles de demostrar de lo que deberían ser, y en particular las conversiones de tipo son lo que más me molesta
En matemáticas normales, los reales son un subconjunto de los complejos, así que cualquier cosa que sea cierta para todos los complejos automáticamente lo es para todos los reales, pero en Lean son tipos distintos y hay que moverse entre ellos mediante aplicaciones inyectivas/operaciones de conversión de tipo, lo que desdibuja el punto central de la prueba
Esto se vuelve especialmente desordenado cuando se acumulan conversiones de tipo como pasar de los naturales a los reales y luego a los complejos
Claro, esto podría ser un problema propio del tema, y en áreas como el álgebra, donde se manejan morfismos explícitos, probablemente se sienta mucho más natural
Es realmente fácil obtener orientación sobre cómo usar mathlib, qué existe y dónde está
Los problemas de conversiones de tipo apiladas por lo general se resuelven con la táctica
norm_castIncluso si no es una pregunta específica, si lo mencionas al pasar o si en tu código se ve un estilo de prueba innecesariamente complicado, pueden sugerirte tácticas que no conocías
Si solo sientes que la formalización es demasiado difícil pero no sabes qué técnica usar, puedes tomar una prueba insatisfactoria que te costó mucho construir, aislarla como ejemplo y pedir a la gente que intente acortarla
Este tipo de preguntas suele ser bien recibido y todos aprenden mucho
Este hilo parece tratar sobre cómo escribir bien matemáticas
Durante décadas he leído, escrito, enseñado, aplicado y publicado matemáticas, y además tengo un doctorado en matemáticas aplicadas
Es cierto que hay problemas en la escritura matemática, y algunas matemáticas están escritas de manera terrible
Pero también hay matemáticas bastante bien escritas
Como mínimo, todos los símbolos deberían definirse antes de usarse, ayuda dar motivación antes de presentar las matemáticas y, a veces, una explicación intuitiva también es útil
Leer con atención matemáticas bien escritas ayuda a aprender escritura matemática
Como ejemplos se pueden mencionar Finite-Dimensional Vector Spaces de Paul R. Halmos, Advanced Calculus de R. Creighton Buck, Mathematical Analysis de Tom M. Apostol, Real Analysis de H. L. Royden, Real and Complex Analysis de Walter Rudin, Probability de Leo Breiman y Mathematical Foundations of the Calculus of Probability de Jacques Neveu
El autor intentó verificar el último teorema de Fermat exactamente en la forma en que se desarrolla en la literatura, y en el proceso descubrió que un lema que sostenía todo un subcampo no es cierto en la forma en que se estaba usando
Aun así, la razón por la que cree que ese campo en general puede salvarse es la confianza en que, si realmente estuviera mal, alguien ya habría encontrado un resultado negativo
Ahora tuvo que encontrar un reemplazo adecuado que sostenga ese campo
Como el autor escribe de manera bastante entretenida, fue una experiencia curiosa: aunque entendí apenas la mitad, se leía con facilidad
Descubrí vitiated como una buena palabra para usar cuando una demostración es refutada o se le encuentra un defecto
Me gusta porque reduce la posibilidad de que se entienda erróneamente que se demostró que la conclusión es falsa, y al mismo tiempo transmite que esa demostración quedó dañada y necesita una nueva prueba o una reparación