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

Résumé technique : Une étude de cas de formalisation du problème du sauterelle utilisant l'API Aristotle

Énoncé du problème
Cet article présente une étude de cas de formalisation du « problème du sauterelle », initialement posé comme le problème 6 de la 50e Olympiade mathématique internationale (OMI 2009). Le théorème énonce que pour tout ensemble de $n$ entiers positifs distincts $\{a_1, \dots, a_n\}$ et tout ensemble $M$ de $n-1$ entiers positifs (où la somme totale $\sum a_i \notin M$), il existe une permutation $\sigma$ des sauts telle qu'aucune somme partielle intermédiaire $S_k = \sum_{i=1}^k a_{\sigma(i)}$ ne tombe dans $M$. Le problème est noté pour sa difficulté historique, ayant obtenu la moyenne la plus basse parmi tous les problèmes de l'OMI 2009, et nécessite un raisonnement combinatoire non trivial impliquant des permutations et des ensembles interdits.

Méthodologie
L'étude utilise l'API Aristotle, un système de preuve de théorèmes automatisé qui combine une recherche guidée par des modèles de langage, une génération de lemmes informels et une formalisation au sein de l'assistant de preuves Lean 4 (en utilisant Mathlib). Les auteurs ont fourni un prompt spécifique à l'API Aristotle demandant une preuve rigoureuse et complète du problème du sauterelle, interdisant explicitement de citer le problème comme un théorème connu et exigeant la construction d'une permutation valide.

L'artefact résultant est un projet Lean 4 contenant une version généralisée du théorème (permettant $|M| < n$ plutôt que strictement $n-1$, et autorisant $0 \in M$). Les auteurs ont effectué une inspection granulaire du code généré pour distinguer les déclarations entièrement vérifiées par la machine de celles contenant des espaces réservés de preuve non résolus (sorry).

Résultats clés et composants vérifiés
Le développement Lean généré n'a pas produit une preuve complète du théorème principal. Il a plutôt abouti à un artefact hybride composé de quatre lemmes d'aide entièrement vérifiés et d'un théorème principal non résolu :

1. Composants locaux vérifiés :

   • PS last : Vérifie que la dernière somme partielle est égale à la somme totale des sauts.
   • PS swap : Vérifie qu'une transposition adjacente de sauts n'affecte que la somme partielle intermédiaire spécifique à cette position, laissant toutes les autres inchangées.
   • PS swap eq : Vérifie la forme algébrique de la somme partielle modifiée après un échange ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$).
   • maximizer swap in M : Vérifie un argument de maximalité locale. Il établit que si une permutation maximise une fonction de score spécifique $G(\sigma)$, et qu'une somme partielle à une position échangeable est dans $M$, alors la valeur résultant de l'échange doit également être dans $M$.

2. Composant global non résolu :

   • Le théorème principal, grasshopper, est clos directement par un seul sorry.
   • Le résumé de la sortie d'Aristotle identifie l'étape manquante comme un argument de comptage global. Alors que les lemmes locaux établissent que des échanges spécifiques imposent l'appartenance à $M$, le système n'a pas réussi à coordonner ces faits pour prouver qu'ils génèrent au moins $n$ valeurs interdites distinctes, ce qui contredirait l'hypothèse $|M| < n$. Le code source Lean ne réduit pas le théorème principal à un lemme de comptage séparé et encodé ; l'écart demeure une obligation non prouvée.

Contributions
L'article apporte deux contributions principales :

1. Un artefact reproductible : Il fournit une tentative de formalisation en Lean 4 inspectable et reproductible d'un problème de combinatoire olympique difficile utilisant l'API Aristotle, incluant le code source complet et les journaux d'exécution.
2. Une analyse précise des limites de l'IA : Il offre une dissection détaillée du « statut probatoire » des preuves générées par l'IA. L'étude démontre que les systèmes d'IA peuvent vérifier avec succès des étapes de raisonnement locales, algébriques et basées sur des échanges, tout en échouant à exécuter la comptabilité combinatoire globale requise pour clore le théorème principal.

Signification et affirmations
L'article soutient que la distinction entre « déclarations vérifiées » et « déclarations closes par sorry » est cruciale pour l'interprétation de la preuve de théorèmes assistée par l'IA. La signification de cette étude de cas réside dans sa démonstration que la recherche de preuves locale peut réussir tandis que le raisonnement global reste non résolu.

Les auteurs soulignent qu'une compilation réussie d'un fichier Lean contenant un sorry est une preuve insuffisante d'une preuve achevée. L'artefact sert d'exemple préventif : bien que les outils d'IA puissent générer des développements mathématiques substantiels et vérifiés (tels que les quatre lemmes d'aide), ils peuvent toujours laisser le moteur logique central de la preuve (la contradiction globale) non implémenté. L'article conclut qu'une formalisation assistée par l'IA digne de confiance nécessite une inspection rigoureuse des obligations de preuve et des dépendances, plutôt qu'une reliance sur la simple présence de code généré.