-
Proyecto Xena y el último teorema de Fermat
- El proyecto Xena tiene como objetivo formalizar las matemáticas en computadoras. Esto busca que, si ocurre una revolución de la IA en matemáticas, las computadoras puedan ayudar a ampliar la frontera de la teoría moderna de números.
-
Formalización del último teorema de Fermat
- Se está trabajando en demostrar el último teorema de Fermat (FLT) en una computadora. En este proceso, una tarea principal es enseñarle a la computadora el teorema R=T.
- En lugar de la prueba original de Wiles, se busca formalizar una demostración moderna, generalizada y simplificada.
-
Cohomología cristalina y estructuras de potencias divididas
- La cohomología cristalina es una teoría desarrollada en las décadas de 1960 y 1970, y cumple un papel importante en la formalización matemática.
- Las estructuras de potencias divididas son un concepto necesario para enseñarle cohomología cristalina a la computadora.
-
El problema de la documentación matemática humana
- Queda en evidencia la falta de precisión en la documentación matemática. Aunque es algo conocido entre especialistas, muchas veces no está bien documentado.
- El trabajo de formalización puede ayudar a resolver estos problemas.
-
La importancia de la formalización
- Formalizar las matemáticas es un paso importante para que las máquinas puedan construir argumentos matemáticos por sí solas.
- Muchos matemáticos no sienten la necesidad de la formalización, pero esta es esencial para reducir errores humanos.
-
Conclusión
- En una presentación reciente se resolvió el problema de formalizar las potencias divididas. Esto significa que el proyecto volvió a encaminarse.
1 comentarios
Opiniones en Hacker News
Recuerda su experiencia en la escuela de posgrado escribiendo código rápido para ayudar con la conjetura de Birch y Swinnerton-Dyer. Cuando dijo en un seminario que quería encontrar un contraejemplo, los expertos se enojaron. No entendía la profundidad de las matemáticas, pero eso despertó su curiosidad.
Se alegra del desarrollo del formalismo en matemáticas. Como programador, esto hace que las matemáticas sean más accesibles. La inquietud por la falta de formalismo debe enfrentarse con curiosidad.
Los matemáticos suelen omitir detalles con frecuencia. Si se quiere una demostración rigurosa, hace falta la ayuda de un experto. Las matemáticas modernas están sobre una base inestable.
Recuerda el proceso por el cual Andrew Wiles demostró el FLT. La forma de demostrar de los años 90 se siente antigua.
Destaca la falta de documentación en las matemáticas modernas. Es necesario reducir errores mediante sistemas formales. Es importante enseñar argumentos matemáticos a las máquinas.
Explica la diferencia entre los roles de diseñador UI/UX y desarrollador. El diseño y el desarrollo requieren formas de pensar distintas.
Espera que demostradores de teoremas como Lean se conviertan en herramientas importantes en matemáticas.
Le parece interesante revisar código de Lean. El enunciado final de la demostración funciona como una prueba unitaria.
Plantea la duda de si es posible que conceptos matemáticos usados durante décadas hayan estado equivocados.
Presenta la palabra "vitiated" y menciona que es útil para usarla cuando una demostración es incorrecta.
Menciona la brecha entre matemáticos e ingenieros, y espera que también hagan falta mejoras de rendimiento cuando las máquinas resuelvan matemáticas.
Expresa decepción por el estado de la literatura matemática. Espera que haya problemas en la literatura de teoría de números entre los años 60 y 90. Cuanto más pequeña es una comunidad de expertos, más fácil es que los errores pasen desapercibidos.