PaperFormalizer convierte artículos en LaTeX en código Lean verificado, con el autor en el circuito

Un equipo de Stanford propone un método que pretende convertir la verificación formal de artículos matemáticos en una parte rutinaria de la preparación de una publicación. PaperFormalizer, lanzado por Jiyuan Tan, Vasilis Syrgkanis y Jose Blanchet, transforma el código fuente LaTeX en una versión del trabajo verificada con Lean. Funciona como un pipeline agéntico dentro de Claude Code o Codex. La idea clave: incluso un artículo revisado con esmero puede contener pequeños huecos en las demostraciones o en la formulación de los supuestos, y quien mejor puede cerrarlos es el propio autor, con la ayuda de la máquina.

Un pipeline de LaTeX a Lean

El proceso empieza por el código fuente. PaperFormalizer transcribe el artículo a un grafo de dependencias de enunciados: qué lemas hacen falta para los teoremas y qué se apoya en qué. Después, cada enunciado pasa una auditoría en lenguaje natural según tres ejes: fidelidad al sentido original, ambigüedad y corrección. Solo entonces el sistema formaliza los enunciados y los demuestra en Lean.

Para las demostraciones, el pipeline recurre a varias fuentes:

• Mathlib, la principal biblioteca matemática de Lean;
• bibliotecas de dominio opcionales para un área concreta;
• el conjunto personal de herramientas del autor, es decir, sus propios lemas y definiciones.

Este conjunto se va acumulando. Cuantos más artículos pasa el autor por el sistema, más bloques listos hay disponibles para el siguiente.

El autor decide qué afirma el artículo

La autoformalización suele adolecer de una sustitución silenciosa del sentido. Un modelo puede demostrar un teorema formalmente impecable que no dice lo que el autor quería decir. Los creadores de PaperFormalizer parten de que solo el autor sabe qué debe significar un enunciado y cuál es la mejor manera de cerrar una laguna de formalización.

Por eso el sistema sigue varias reglas:

• si un enunciado admite más de una lectura, el pipeline se detiene y plantea una pregunta;
• cada corrección se presenta en lenguaje natural y en símbolos TeX como una propuesta que se puede aceptar, rechazar o reorientar;
• cualquier decisión que pueda cambiar lo declarado en el artículo queda en manos del autor.

A diferencia de los sistemas que intentan formalizar trabajos ajenos de forma íntegra y autónoma, aquí el humano actúa como árbitro del sentido y la máquina asume la mecánica pesada de las demostraciones.

Qué obtiene el autor a la salida

El resultado consta de tres partes:

• una versión anotada y corregida del artículo;
• un informe de todos los cambios realizados;
• código Lean en el que cada declaración está vinculada al enunciado que formaliza.

Ese último vínculo es importante para el lector. Se puede abrir cualquier teorema del texto y ver el objeto Lean verificado que le corresponde, en lugar de buscar la correspondencia a mano.

Una biblioteca común de trabajos verificados

Los autores proponen también una capa de ecosistema. Los investigadores pueden publicar artículos verificados en el sitio paperformalizer.org, y quienes construyan sobre esos resultados podrán reutilizar el código Lean ya hecho. Eso reduce el coste de formalizar el siguiente trabajo en la misma área: las definiciones y los lemas necesarios ya existen y están verificados.

La herramienta está publicada en GitHub, en el repositorio Jiyuan-Tan/PaperFormalizer. El trabajo salió el 22 de octubre de 2026 y entró en la selección diaria de Hugging Face Papers; en su página, la organización figura como Stanford University.

Utilidad práctica para los investigadores

Para matemáticos y teóricos de la estadística, la economía y el aprendizaje automático, cuyas conclusiones se sostienen sobre demostraciones, es una forma de obtener una verificación independiente antes de enviar el trabajo a una revista. Resulta especialmente útil donde los errores en los supuestos pasan inadvertidos en la revisión por pares. La barrera de entrada es más baja que la de la formalización manual en Lean: hacen falta el código fuente LaTeX, acceso a Claude Code o Codex y disposición a responder a las preguntas del sistema.

También conviene ser cautos. El pipeline comprueba que el enunciado formal está demostrado, pero sigue siendo una persona quien confirma que la formalización se corresponde con la intención. Por eso la calidad del resultado depende de la atención del autor justo en los puntos en los que el sistema se detiene y pregunta.