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

Technische Samenvatting: Een Formalisatiecasestudie van het Sprinkhaanprobleem met de Aristotle API

Probleemstelling
Dit artikel presenteert een formalisatiecasestudie van het "Sprinkhaanprobleem", oorspronkelijk gesteld als Probleem 6 van de 50e Internationale Wiskunde Olympiade (IMO 2009). De stelling luidt dat voor elke verzameling van $n$ verschillende positieve gehele getallen $\{a_1, \dots, a_n\}$ en een verzameling $M$ van $n-1$ positieve gehele getallen (waarbij de totale som $\sum a_i \notin M$), er een permutatie $\sigma$ van de sprongen bestaat zodanig dat geen enkele tussenliggende partiële som $S_k = \sum_{i=1}^k a_{\sigma(i)}$ in $M$ terechtkomt. Het probleem staat bekend om zijn historische moeilijkheidsgraad, met het laagste gemiddelde score onder alle IMO-problemen van 2009, en vereist niet-triviale combinatorische redenering die permutaties en verboden verzamelingen omvat.

Methodologie
De studie maakt gebruik van de Aristotle API, een geautomatiseerd stellingbewijssysteem dat zoekopdrachten geleid door taalmodellen, het genereren van informele lemma's en formalisatie binnen de Lean 4 bewijshulp (met Mathlib) combineert. De auteurs hebben een specifieke prompt aan de Aristotle API gegeven waarin werd gevraagd om een rigoureus, volledig bewijs van het Sprinkhaanprobleem, waarbij expliciet werd verboden om het probleem te citeren als een bekend stelling en waarbij werd geëist dat een geldige permutatie werd geconstrueerd.

Het resulterende artefact is een Lean 4-project dat een gegeneraliseerde versie van de stelling bevat (waarbij $|M| < n$ wordt toegestaan in plaats van strikt $n-1$, en waarbij $0 \in M$ wordt toegestaan). De auteurs hebben een gedetailleerde inspectie uitgevoerd van de gegenereerde code om onderscheid te maken tussen declaraties die volledig machine-geverifieerd zijn en die welke onopgeloste bewijsplaatsaanduidingen (sorry) bevatten.

Belangrijkste Resultaten en Geverifieerde Componenten
De gegenereerde Lean-ontwikkeling leverde geen volledig bewijs van de hoofdstelling op. In plaats daarvan resulteerde het in een hybride artefact bestaande uit vier volledig geverifieerde helper-lemma's en één onopgeloste hoofdstelling:

1. Geverifieerde Lokale Componenten:

   • PS last: Geverifieerd dat de laatste partiële som gelijk is aan de totale som van de sprongen.
   • PS swap: Geverifieerd dat een aangrenzende transpositie van sprongen alleen de specifieke tussenliggende partiële som op die positie beïnvloedt, terwijl alle andere ongewijzigd blijven.
   • PS swap eq: Geverifieerd de algebraïsche vorm van de gewijzigde partiële som na een verwisseling ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$).
   • maximizer swap in M: Geverifieerd een lokaal maximaliteitsargument. Het stelt vast dat als een permutatie een specifieke scoresfunctie $G(\sigma)$ maximaliseert, en een partiële som op een verwisselbare positie in $M$ zit, dan moet de waarde die resulteert uit de verwisseling ook in $M$ zitten.

2. Onopgeloste Globale Component:

   • De hoofdstelling, grasshopper, wordt direct afgesloten met een enkele sorry.
   • De Aristotle-outputsamenvatting identificeert de ontbrekende stap als een globaal telargument. Hoewel de lokale lemma's vaststellen dat specifieke verwisselingen lidmaatschap in $M$ afdwingen, slaagde het systeem er niet in om deze feiten te coördineren om te bewijzen dat ze ten minste $n$ verschillende verboden waarden genereren, wat in strijd zou zijn met de aanname $|M| < n$. De Lean-broncode reduceert de hoofdstelling niet tot een apart, gecodeerd tellemma; de kloof blijft een onbewezen verplichting.

Bijdragen
Het artikel levert twee primaire bijdragen:

1. Een Reproduceerbaar Artefact: Het biedt een inspecteerbare, reproduceerbare Lean 4-formalisatiepoging van een moeilijk olympiade-combinatoriekprobleem met behulp van de Aristotle API, inclusief de volledige broncode en uitvoerlogs.
2. Een Precieze Analyse van AI-beperkingen: Het biedt een gedetailleerde dissectie van de "evidentiële status" van door AI gegenereerde bewijzen. De studie toont aan dat AI-systemen lokaal, algebraïsch en op uitwisseling gebaseerde redeneerstappen succesvol kunnen verifiëren, terwijl ze falen in het uitvoeren van de globale combinatorische administratie die nodig is om de hoofdstelling af te sluiten.

Betekenis en Aanspraken
Het artikel betoogt dat het onderscheid tussen "geverifieerde declaraties" en "declaraties afgesloten met sorry" kritiek is voor de interpretatie van door AI ondersteund stellingbewijzen. De betekenis van deze casestudie ligt in de demonstratie dat lokale bewijzingszoekopdrachten kunnen slagen terwijl globale redenering onopgelost blijft.

De auteurs benadrukken dat een succesvolle compilatie van een Lean-bestand dat sorry bevat, onvoldoende bewijs is van een voltooid bewijs. Het artefact dient als een waarschuwend voorbeeld: hoewel AI-tools aanzienlijke, geverifieerde wiskundige ontwikkelingen kunnen genereren (zoals de vier helper-lemma's), kunnen ze de kernlogische motor van het bewijs (de globale tegenstrijdigheid) nog steeds onuitgevoerd laten. Het artikel concludeert dat betrouwbare door AI ondersteunde formalisatie een rigoureuze inspectie van bewijsverplichtingen en afhankelijkheden vereist, in plaats van vertrouwen op louter de aanwezigheid van gegenereerde code.