Proponen una revista que exigirá verificar en Lean las pruebas matemáticas, ante el avance de la IA

Contenido elaborado con ayuda de inteligencia artificial. Las fuentes se indican cuando corresponde.

La expansión de las demostraciones asistidas por IA plantea una pregunta: cómo comprobar que son correctas. Shaoming Guo y varios colegas proponen una revista que exigiría verificar formalmente las pruebas en Lean antes de aceptar los artículos. La propuesta aparece como texto invitado en el blog de Terence Tao.

Comprender, además de llegar primero

El proyecto plantea dar más valor a cuánto ayuda un trabajo a entender sus resultados y demostraciones que a la prioridad del descubrimiento. Mantendría también valores tradicionales como el acceso abierto.

Qué aporta Lean

Lean es un lenguaje y asistente de demostración que permite escribir pruebas formales comprobables por ordenador. Guo explica que el uso creciente de modelos de lenguaje aumenta la preocupación por errores sutiles difíciles de detectar.

Es una propuesta, no una revista ya abierta

El texto invita a debatir el proyecto y otras formas de publicación científica. No anuncia nombre de la revista, equipo editorial completo ni fecha de apertura. Tampoco supone que todos los resultados producidos con IA sean erróneos: la propuesta busca elevar el nivel de comprobación.

Propuesta fechada en el blog: 17/10/2026. Publicación en GeneratIvA: 18/10/2026.

Fuentes: Publicación original · Confirmación y contexto.

Fotografía contextual de una pizarra, publicada en febrero de 2026; no corresponde al proyecto de revista ni muestra una prueba verificada en Lean. Erwan Hesry / Unsplash. Procedencia de la imagen. Licencia Unsplash.