Tweet
En 2023 nació el proyecto LANA (Lean for ANAbelian geometry) del japonés Centro de Matemáticas ZEN (ZMC). Su objetivo era verificar de forma automática en Lean la (supuesta) demostración de Mochizuki, lo que requiere desarrollar una librería en Lean con toda la geometría anabelina y la teoría de Teichmüller interuniversal (IUT). El 20 de julio de 2026 se ha publicado su primer informe oficial de resultados. Como era de esperar, tras dos años de duro trabajo, el proyecto LANA está atascado en la transición del teorema 3.11 al corolario 3.12
- Si esta es tu primera visita asegúrate de revisar las FAQ en el enlace anterior. En necesario registrase antes de poder publicar. Para empezar a ver mensajes, selecciona el foro que quieres visitar de la lista inferior.
