🤖 AI

Case study: proving sqrt(2) irrational with LPTP and an LLM

Este artículo presenta un estudio de caso que demuestra cómo un LLM, guiado por definiciones básicas de programación lógica y verificado por el demostrador de teoremas LPTP, puede generar con éxito una prueba formal completa y legible por humanos de la irracionalidad de la raíz cuadrada de 2.

Autores originales: Fred Mesnard, Étienne Payet, Wim Vanhoof

Publicado 2026-07-24

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Fred Mesnard, Étienne Payet, Wim Vanhoof

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que eres un detective tratando de resolver un misterio que ha desconcertado a los humanos durante más de dos mil años: ¿Es la raíz cuadrada de 2 un número "racional"? En el mundo de las matemáticas, un número racional es como una fracción perfecta, una rebanada limpia de un pastel (como 3/4 o 5/2). Un número irracional es un decimal desordenado y sin fin que nunca puede escribirse como una fracción simple. La raíz cuadrada de 2 es la longitud de la diagonal de un cuadrado con lados de longitud 1, y los matemáticos antiguos demostraron que es desordenada: no puede ser una fracción.

Ahora, imagina que tienes dos herramientas muy diferentes para ayudarte a resolver esto. La primera es un árbitro súper estricto y robótico llamado LPTP. Habla un lenguaje muy preciso y lógico (basado en Prolog) y solo aceptará una prueba si cada uno de sus pasos es matemáticamente perfecto. Si cometes incluso el más mínimo error, golpea el mazo y dice: "No, inválido". La segunda herramienta es un Modelo de Lenguaje Grande (LLM), que es como un estudiante súper inteligente y creativo que ha leído casi todo lo escrito. Este estudiante es excelente adivinando el siguiente paso en una historia o un problema matemático, pero a veces "alucina", inventando hechos que suenan bien pero que son falsos.

La gran pregunta para los científicos hoy en día es: ¿Podemos unir estos dos? ¿Podemos dejar que el estudiante creativo haga el trabajo pesado de escribir la prueba, mientras el árbitro estricto revisa cada oración para asegurarse de que el estudiante no esté mintiendo? Este artículo explora exactamente esa asociación, utilizando el antiguo misterio de la raíz cuadrada de 2 como el caso de prueba.

El Gran Equipo de Verificación de Pruebas

En este artículo, los autores se propusieron ver si podían usar una IA moderna (específicamente, un modelo llamado Claude) para ayudar a demostrar que la raíz cuadrada de 2 es irracional, pero con un giro: la prueba tenía que estar escrita en un formato muy específico y estricto que el árbitro robótico (LPTP) pudiera entender y verificar. No querían simplemente que la IA dijera "es verdad"; querían que la IA escribiera la lógica paso a paso real, que el árbitro luego calificaría.

La historia comienza con una idea simple. Para demostrar que la raíz cuadrada de 2 es irracional, normalmente se asume lo contrario: que es una fracción hecha de dos números enteros, $p$ y $q$ , que no comparten ningún factor común (son "primos entre sí" o coprimos). Si haces las matemáticas, eventualmente te encuentras con una contradicción donde ambos números deben ser pares, lo que significa que sí comparten un factor (2). Esto rompe la regla de que eran coprimos, demostrando que la suposición original era errónea.

Los autores intentaron que la IA escribiera esta prueba en el lenguaje estricto de LPTP. Al principio, la IA era como un estudiante que conoce la historia pero no sabe escribir el ensayo en el formato requerido. Intentaba saltarse pasos o dar saltos lógicos que el árbitro no aceptaría.

Aquí es donde ocurrió el trabajo en equipo. Los autores establecieron un ciclo de retroalimentación:

La IA intenta escribir un paso de la prueba.
El árbitro (LPTP) la verifica.
Si el árbitro encuentra un error, señala la línea exacta donde la lógica falló.
Los autores le muestran ese error a la IA.
La IA lo intenta de nuevo, corrigiendo el error específico.

Este proceso fue como un juego de "caliente y frío". El árbitro no solo decía "incorrecto"; decía: "Cometiste un error en el paso 4", permitiendo que la IA corrigiera su rumbo.

Los Resultados: Una Victoria Parcial

El experimento fue un éxito, pero con algunas salvedades. La IA fue capaz de demostrar por sí sola muchas de las partes más pequeñas y fáciles del rompecabezas. Por ejemplo, demostró con éxito que "si un número es par, su cuadrado es par" o que "2 veces un número es par". Los autores llaman a estas "lemas" (pequeñas pruebas auxiliares). La IA acertó en estas, incluso llegando a proponer nuevas ideas auxiliares que los humanos no habían pensado.

Sin embargo, para la parte más difícil de la prueba —la lógica específica que muestra por qué la raíz cuadrada de 2 no puede ser una fracción— la IA se quedó estancada. No pudo encontrar el camino correcto por sí sola. Por lo tanto, los autores humanos tuvieron que intervenir para darle una "pista" o incluso escribir la estructura principal de la prueba ellos mismos, pidiéndole a la IA que llenara los espacios más pequeños.

Al final, produjeron una prueba formal completa de que la raíz cuadrada de 2 es irracional. Esta prueba fue escrita parcialmente por la IA y totalmente verificada por el árbitro robótico. El árbitro le dio una calificación de aprobado, confirmando que la lógica era sólida.

Lo Que Esto Significa

El artículo no afirma que la IA pueda resolver ahora todos los problemas matemáticos por sí sola. De hecho, los autores muestran explícitamente que la IA no puede hacerlo sola; sin la guía humana y la verificación estricta del árbitro, la IA probablemente habría producido una prueba falsa o rota.

En cambio, el artículo sugiere una nueva forma de trabajar: la IA como redactora de borradores, los humanos como editores y las herramientas formales como verificadores de hechos. La IA es rápida y creativa, generando ideas y llenando detalles, mientras que la herramienta formal (LPTP) actúa como un ojo que no parpadea, detectando alucinaciones y errores.

Los autores también probaron otras herramientas matemáticas automatizadas (llamadas ATP) para ver si podían hacer el trabajo más rápido. Estas herramientas eran rápidas y gratuitas, pero producían pruebas difíciles de leer para los humanos y que no podían añadirse fácilmente a la biblioteca de matemáticas verificadas. El enfoque de la IA, aunque más lento y que requiere ayuda humana, produjo pruebas legibles y que podían almacenarse de forma segura para uso futuro.

En resumen, este artículo muestra que no tenemos que elegir entre la intuición humana y la precisión de la máquina. Al dejar que la IA haga el trabajo pesado de redactar los borradores y que las herramientas estrictas se encarguen de calificar, podemos construir un sistema donde la IA nos ayude a demostrar verdades matemáticas complejas, siempre y cuando mantengamos a un humano al mando para dirigir el barco y a un árbitro estricto para revisar el mapa. La raíz cuadrada de 2 sigue siendo irracional, pero ahora tenemos una nueva forma colaborativa de demostrarlo.

Resumen Técnico: Estudio de Caso para Probar la Irracionalidad de $\sqrt{2}$ con LPTP y un LLM

Planteamiento del Problema
El artículo aborda el desafío de probar formalmente que la raíz cuadrada de 2 es irracional dentro del contexto de la Programación Lógica (LP). Específicamente, los autores pretenden demostrar que no existen dos números naturales coprimos $p$ y $q$ tales que $p^2 = 2q^2$ . Si bien este es un resultado matemático clásico, los motores de programación lógica basados en resolución estándar (como Prolog) no pueden proporcionar una respuesta negativa a la consulta correspondiente debido a que el espacio de búsqueda sobre los números naturales es infinito. Los autores buscan cerrar esta brecha utilizando el sistema LPTP (Logic Program Theorem Prover) para generar una prueba formal y evaluar hasta qué punto un Modelo de Lenguaje de Gran Escala (LLM) puede asistir en la construcción de dicha prueba.

Metodología
Los autores emplean un enfoque híbrido que combina el sistema de verificación formal LPTP con un LLM (específicamente Claude Opus 4.5 de Anthropic).

Marco Formal (LPTP):
- LPTP se utiliza para verificar propiedades de programas lógicos basados en la lógica de primer orden y la completitud de Clark.
- El sistema distingue entre éxito, fallo y terminación de predicados utilizando operadores específicos ( $S$ , $F$ , $T$ ) y admite esquemas de inducción para predicados recursivos.
- El lenguaje de prueba se basa en la deducción natural, garantizando la legibilidad para humanos.
- Los autores definen el problema utilizando predicados de Prolog puro para números naturales (aritmética de Peano), suma, multiplicación y MCD (Máximo Común Divisor).
Estrategia de Integración de LLM:
- Aprendizaje en Contexto (In-Context Learning): El LLM recibe el manual de usuario de LPTP (PDF) y dos librerías básicas (números de Peano y listas) que contienen código Prolog y pruebas existentes.
- Bucle de Retroalimentación Iterativo: Los autores presentan lemas al LLM en sintaxis LPTP (o lenguaje natural). El LLM genera un intento de prueba, que es inmediatamente enviado al verificador de pruebas de LPTP.
- Corrección de Errores: Si el verificador de LPTP rechaza la prueba, reporta el primer paso de derivación incorrecto. Este error específico se introduce de nuevo al LLM para refinar la prueba.
- Supervisión Humana: Un desarrollador humano gestiona el orden de los lemas, decide cuándo abandonar bucles improductivos y proporciona pistas de alto nivel o la estructura de la prueba para pasos difíciles.
Herramientas Auxiliares:
- Los autores también utilizaron Probadores Automáticos de Teoremas (ATP) de lógica de primer orden (FOL) convencionales como Vampire y E, traduciendo los axiomas de LPTP a sintaxis FOF. Estos se utilizaron para verificar lemas de forma independiente, aunque sus pruebas basadas en resolución no podían integrarse directamente en el marco de deducción natural de LPTP.

Contribuciones Claves y Resultados

Construcción de la Prueba: El equipo construyó con éxito una prueba completa y verificada por máquina de la irracionalidad de $\sqrt{2}$ en LPTP. La prueba fue generada parcialmente por el LLM y validada totalmente por el verificador de LPTP.
Generación de Lemas:
- El LLM probó con éxito varios lemas auxiliares de forma directa (por ejemplo, $2^2=4$ , propiedades de números pares/impares) o tras unas pocas iteraciones de corrección de errores (por ejemplo, lemas de simplificación).
- Para el lema más complejo, evenpp:evenp (probar que si el cuadrado de un número es par, el número mismo es par), el LLM falló inicialmente. Los autores proporcionaron una pista en lenguaje natural delineando la prueba por casos (par vs. impar), tras lo cual el LLM generó con éxito la prueba formal.
- El teorema principal (sqrt2:irrational) requirió que los autores proporcionaran el esqueleto de la prueba; el LLM completó entonces los pasos necesarios y los lemas auxiliares.
Comparación con ATP: Mientras que los ATP pudieron probar 9 de los 12 lemas en la versión final, fallaron al intentar probar el teorema principal dentro del tiempo límite de 20 segundos, debido probablemente a la expansión del espacio de búsqueda. Crucialmente, las pruebas de los ATP no podían convertirse directamente en las pruebas de deducción natural requeridas por LPTP.
Gestión de Dependencias: El artículo detalla el grafo de dependencia de los lemas, mostrando cómo la capacidad del LLM para probar propiedades simples (como nat:natsquare o sqr2:4) fue esencial para probar propiedades de mayor nivel.

Significancia y Reivindicaciones
Los autores afirman que este trabajo representa una de las primeras interacciones entre LPTP y un LLM. Su contribución principal es demostrar un flujo de trabajo semiautomatizado donde:

El Verificador de Pruebas es Central: El verificador de LPTP actúa como el filtro crítico contra las alucinaciones del LLM. Proporciona retroalimentación precisa (el primer paso incorrecto), permitiendo que el LLM se autocorrija de manera efectiva.
Roles Complementarios: Los ATP son rápidos y locales, pero producen pruebas en un formato (resolución/superposición) incompatible con la deducción natural de LPTP. Los LLM, guiados por el verificador, pueden generar pruebas en el formato correcto, aunque requieren guía humana para los pasos estructurales complejos.
Viabilidad para LP: El estudio valida que los LLM pueden integrarse eficazmente en la verificación de propiedades de Programación Lógica, siempre que exista un bucle de verificación de pruebas riguroso.

El artículo concluye de manera modesta, señalando que, si bien el LLM no pudo generar toda la estructura de la prueba de forma autónoma para el teorema principal, manejó con éxito los pasos lógicos granulares una vez definida la estructura. Esto allana el camino para futuros enfoques potenciados por IA para probar propiedades de Prolog, con los autores planeando evaluar esta combinación en un conjunto más amplio de problemas de verificación.

El Gran Equipo de Verificación de Pruebas

Los Resultados: Una Victoria Parcial

Lo Que Esto Significa

Más como este