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

Technisches Fazit: Eine Formalisierungsfallstudie des Heuschrecken-Problems unter Verwendung der Aristotle-API

Problemstellung
Diese Arbeit präsentiert eine Formalisierungsfallstudie des „Heuschrecken-Problems", das ursprünglich als Problem 6 der 50. Internationalen Mathematik-Olympiade (IMO 2009) formuliert wurde. Der Satz besagt, dass für jede Menge von $n$ verschiedenen positiven ganzen Zahlen $\{a_1, \dots, a_n\}$ und eine Menge $M$ von $n-1$ positiven ganzen Zahlen (wobei die Gesamtsumme $\sum a_i \notin M$ ist), eine Permutation $\sigma$ der Sprünge existiert, sodass keine intermediate Teilsumme $S_k = \sum_{i=1}^k a_{\sigma(i)}$ in $M$ landet. Das Problem ist für seine historische Schwierigkeit bekannt, da es die niedrigste durchschnittliche Punktzahl unter allen IMO-Problemen des Jahres 2009 aufwies, und erfordert nicht-triviale kombinatorische Überlegungen, die Permutationen und verbotene Mengen betreffen.

Methodik
Die Studie nutzt die Aristotle-API, ein automatisches Theorembeweissystem, das suchbasierte Verfahren mit Sprachmodellen, die Generierung informeller Lemmata und die Formalisierung innerhalb des Lean 4-Beweisassistenten (unter Verwendung von Mathlib) kombiniert. Die Autoren gaben der Aristotle-API eine spezifische Aufforderung, einen rigorosen, vollständigen Beweis des Heuschrecken-Problems zu liefern, wobei sie explizit Zitate des Problems als bekannten Satz untersagten und die Konstruktion einer gültigen Permutation forderten.

Das resultierende Artefakt ist ein Lean-4-Projekt, das eine generalisierte Version des Satzes enthält (die $|M| < n$ statt strikt $n-1$ erlaubt und $0 \in M$ zulässt). Die Autoren führten eine granulare Inspektion des generierten Codes durch, um zwischen Deklarationen zu unterscheiden, die vollständig maschinell verifiziert sind, und solchen, die ungelöste Beweisplatzhalter (sorry) enthalten.

Hauptergebnisse und verifizierte Komponenten
Die generierte Lean-Entwicklung lieferte keinen vollständigen Beweis des Hauptsatzes. Stattdessen entstand ein hybrides Artefakt, bestehend aus vier vollständig verifizierten Hilfslemmata und einem ungelösten Hauptsatz:

1. Verifizierte lokale Komponenten:

   • PS last: Verifiziert, dass die finale Teilsumme der Gesamtsumme der Sprünge entspricht.
   • PS swap: Verifiziert, dass eine benachbarte Transposition von Sprüngen nur die spezifische intermediate Teilsumme an dieser Position beeinflusst und alle anderen unverändert lässt.
   • PS swap eq: Verifiziert die algebraische Form der geänderten Teilsumme nach einem Tausch ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$).
   • maximizer swap in M: Verifiziert ein Argument der lokalen Maximalität. Es stellt fest, dass, wenn eine Permutation eine bestimmte Bewertungsfunktion $G(\sigma)$ maximiert und eine Teilsumme an einer tauschbaren Position in $M$ liegt, der Wert, der sich aus dem Tausch ergibt, ebenfalls in $M$ liegen muss.

2. Ungelöste globale Komponente:

   • Der Hauptsatz grasshopper wird direkt durch ein einzelnes sorry abgeschlossen.
   • Die Aristotle-Ausgabe-Zusammenfassung identifiziert den fehlenden Schritt als ein globales Zählargument. Während die lokalen Lemmata feststellen, dass bestimmte Tausche die Mitgliedschaft in $M$ erzwingen, gelang es dem System nicht, diese Fakten zu koordinieren, um zu beweisen, dass sie mindestens $n$ verschiedene verbotene Werte erzeugen, was der Annahme $|M| < n$ widersprechen würde. Die Lean-Quelle reduziert den Hauptsatz nicht auf ein separates, kodiertes Zähllemma; die Lücke bleibt eine unbewiesene Verpflichtung.

Beiträge
Die Arbeit leistet zwei primäre Beiträge:

1. Ein reproduzierbares Artefakt: Sie bietet einen überprüfbaren, reproduzierbaren Formalisierungsversuch eines schwierigen kombinatorischen Problems der Mathematik-Olympiade unter Verwendung der Aristotle-API in Lean 4, einschließlich des vollständigen Quellcodes und der Laufprotokolle.
2. Eine präzise Analyse von KI-Grenzen: Sie bietet eine detaillierte Zerlegung des „evidentiären Status" von KI-generierten Beweisen. Die Studie zeigt, dass KI-Systeme lokale, algebraische und austauschbasierte Beweisschritte erfolgreich verifizieren können, während sie scheitern, die für den Abschluss des Hauptsatzes erforderliche globale kombinatorische Buchhaltung durchzuführen.

Bedeutung und Behauptungen
Die Arbeit argumentiert, dass die Unterscheidung zwischen „verifizierten Deklarationen" und „Deklarationen, die durch sorry abgeschlossen sind", für die Interpretation KI-gestützten Theorembeweisens entscheidend ist. Die Bedeutung dieser Fallstudie liegt in ihrer Demonstration, dass lokale Beweissuche erfolgreich sein kann, während globale Überlegungen ungelöst bleiben.

Die Autoren betonen, dass eine erfolgreiche Kompilierung einer Lean-Datei, die sorry enthält, kein ausreichender Beweis für einen abgeschlossenen Beweis ist. Das Artefakt dient als warnendes Beispiel: Während KI-Tools erhebliche, verifizierte mathematische Entwicklungen generieren können (wie die vier Hilfslemmata), lassen sie möglicherweise den Kernlogikmotor des Beweises (den globalen Widerspruch) unausgeführt. Die Arbeit schließt, dass vertrauenswürdige KI-gestützte Formalisierung eine rigorose Inspektion von Beweisverpflichtungen und Abhängigkeiten erfordert, anstatt sich auf das bloße Vorhandensein generierten Codes zu verlassen.