Sesión Lógica y ComputabilidadVerificación automática de novedad matemática con Lean 4
Ayrton Porto
UNICEN e investigación independiente, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
El proceso de revisión en revistas de matemática puede extenderse por meses o años. Buena parte de ese tiempo se dedica a verificar la corrección de los resultados y a determinar si son genuinamente nuevos. AViD Journal aborda este problema: un pipeline que recibe un artículo en LaTeX, formaliza sus enunciados en Lean 4 mediante LLMs, y emite un veredicto de novedad automáticamente.
Comenzaremos con una pequeña introducción a Lean 4. Luego presentaremos AViD en detalle: el parser que extrae entornos matemáticos y ordena dependencias, la arquitectura de formalización con agentes sobre múltiples backends, y el árbol de decisión sobre tres dimensiones — existencia previa en corpus formales (Mathlib, vía Leandex) e informales (TheoremSearch, Matlas), trivialidad por tácticas automáticas de Lean, y distancia estructural entre demostraciones como distancia de Jaccard sobre premisas. El sistema se evaluó sobre artículos reales retirados de arXiv por duplicación declarada. Mencionaremos los obstaculos de su implementación a escala.
Si el tiempo lo permite, mostraremos una ejecución en vivo con un archivo .tex de los participantes (invitamos a acercarlo).
La presentación no asume conocimiento previo de Lean ni de verificación formal.
Referencias
[1] A. Porto, "Beyond Correctness: Toward Automated Novelty Verification with Lean 4", 2026.
[2] K. Kasaura et al., "Discovering New Theorems via LLMs with In-Context Proof Learning in Lean", 2025
[3] L. Alexander et al., "Semantic Search over 9 Million Mathematical Theorems", 2026.
[4] Mathlib Community, "mathlib4". (https://github.com/leanprover-community/mathlib4).