Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

Resumen Técnico: Un Estudio de Caso de Formalización del Problema del Saltamontes Utilizando la API de Aristotle

Enunciado del Problema
Este artículo presenta un estudio de caso de formalización del "Problema del Saltamontes", planteado originalmente como el Problema 6 de la 50ª Olimpiada Matemática Internacional (OMI 2009). El teorema establece que para cualquier conjunto de $n$ enteros positivos distintos $\{a_1, \dots, a_n\}$ y un conjunto $M$ de $n-1$ enteros positivos (donde la suma total $\sum a_i \notin M$), existe una permutación $\sigma$ de los saltos tal que ninguna suma parcial intermedia $S_k = \sum_{i=1}^k a_{\sigma(i)}$ cae en $M$. Se destaca la dificultad histórica del problema, al haber obtenido la puntuación media más baja entre todos los problemas de la OMI 2009, y requiere un razonamiento combinatorio no trivial que involucra permutaciones y conjuntos prohibidos.

Metodología
El estudio utiliza la API de Aristotle, un sistema de demostración automática de teoremas que combina búsqueda guiada por modelos de lenguaje, generación de lemas informales y formalización dentro del asistente de pruebas Lean 4 (utilizando Mathlib). Los autores proporcionaron un prompt específico a la API de Aristotle solicitando una demostración rigurosa y completa del Problema del Saltamontes, prohibiendo explícitamente citar el problema como un teorema conocido y exigiendo la construcción de una permutación válida.

El artefacto resultante es un proyecto Lean 4 que contiene una versión generalizada del teorema (permitiendo $|M| < n$ en lugar de estrictamente $n-1$, y permitiendo $0 \in M$). Los autores realizaron una inspección granular del código generado para distinguir entre declaraciones completamente verificadas por la máquina y aquellas que contienen marcadores de posición de prueba sin resolver (sorry).

Resultados Clave y Componentes Verificados
El desarrollo Lean generado no produjo una demostración completa del teorema principal. En su lugar, dio lugar a un artefacto híbrido compuesto por cuatro lemas auxiliares completamente verificados y un teorema principal sin resolver:

1. Componentes Locales Verificados:

   • PS last: Verificó que la suma parcial final es igual a la suma total de los saltos.
   • PS swap: Verificó que una transposición adyacente de saltos afecta únicamente a la suma parcial intermedia específica en esa posición, dejando todas las demás sin cambios.
   • PS swap eq: Verificó la forma algebraica de la suma parcial modificada después de un intercambio ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$).
   • maximizer swap in M: Verificó un argumento de maximalidad local. Establece que si una permutación maximiza una función de puntuación específica $G(\sigma)$, y una suma parcial en una posición intercambiable está en $M$, entonces el valor resultante del intercambio también debe estar en $M$.

2. Componente Global Sin Resolver:

   • El teorema principal, grasshopper, se cierra directamente mediante un único sorry.
   • El resumen de la salida de Aristotle identifica el paso faltante como un argumento de conteo global. Mientras que los lemas locales establecen que intercambios específicos fuerzan la pertenencia a $M$, el sistema no logró coordinar estos hechos para demostrar que generan al menos $n$ valores prohibidos distintos, lo cual contradiría la suposición $|M| < n$. El código fuente Lean no reduce el teorema principal a un lema de conteo separado y codificado; la brecha permanece como una obligación no probada.

Contribuciones
El artículo hace dos contribuciones principales:

1. Un Artefacto Reproducible: Proporciona un intento de formalización en Lean 4, inspeccionable y reproducible, de un problema difícil de olimpiada de combinatoria utilizando la API de Aristotle, incluyendo el código fuente completo y los registros de ejecución.
2. Un Análisis Preciso de las Limitaciones de la IA: Ofrece una disección detallada del "estado evidencial" de las pruebas generadas por IA. El estudio demuestra que los sistemas de IA pueden verificar con éxito pasos de razonamiento locales, algebraicos y basados en intercambios, mientras que fallan en ejecutar la contabilidad combinatoria global necesaria para cerrar el teorema principal.

Significado y Afirmaciones
El artículo argumenta que la distinción entre "declaraciones verificadas" y "declaraciones cerradas por sorry" es crítica para la interpretación de la demostración de teoremas asistida por IA. El significado de este estudio de caso radica en su demostración de que la búsqueda de pruebas local puede tener éxito mientras que el razonamiento global permanece sin resolver.

Los autores enfatizan que una compilación exitosa de un archivo Lean que contiene sorry es evidencia insuficiente de una prueba completada. El artefacto sirve como un ejemplo de advertencia: aunque las herramientas de IA pueden generar desarrollos matemáticos sustanciales y verificados (como los cuatro lemas auxiliares), aún pueden dejar el motor lógico central de la prueba (la contradicción global) sin implementar. El artículo concluye que una formalización asistida por IA confiable requiere una inspección rigurosa de las obligaciones y dependencias de las pruebas, en lugar de depender de la mera presencia de código generado.