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

Riepilogo Tecnico: Uno Studio di Caso di Formalizzazione del Problema del Grillo con l'API Aristotle

Enunciato del Problema
Questo articolo presenta uno studio di caso di formalizzazione del "problema del grillo", originariamente proposto come Problema 6 della 50ª Olimpiade Internazionale di Matematica (IMO 2009). Il teorema afferma che per qualsiasi insieme di $n$ interi positivi distinti $\{a_1, \dots, a_n\}$ e un insieme $M$ di $n-1$ interi positivi (dove la somma totale $\sum a_i \notin M$), esiste una permutazione $\sigma$ dei salti tale che nessuna somma parziale intermedia $S_k = \sum_{i=1}^k a_{\sigma(i)}$ atterri in $M$. Il problema è noto per la sua difficoltà storica, avendo ottenuto il punteggio medio più basso tra tutti i problemi dell'IMO 2009, e richiede un ragionamento combinatorio non banale che coinvolge permutazioni e insiemi proibiti.

Metodologia
Lo studio utilizza l'API Aristotle, un sistema di dimostrazione automatica di teoremi che combina una ricerca guidata da modelli linguistici, la generazione informale di lemmi e la formalizzazione all'interno dell'assistente di dimostrazione Lean 4 (utilizzando Mathlib). Gli autori hanno fornito un prompt specifico all'API Aristotle richiedendo una dimostrazione rigorosa e completa del problema del grillo, vietando esplicitamente la citazione del problema come teorema noto e demandando la costruzione di una permutazione valida.

L'artefatto risultante è un progetto Lean 4 contenente una versione generalizzata del teorema (che consente $|M| < n$ invece di strettamente $n-1$, e permette $0 \in M$). Gli autori hanno eseguito un'ispezione granulare del codice generato per distinguere tra dichiarazioni completamente verificate dalla macchina e quelle contenenti segnaposto di prova irrisolti (sorry).

Risultati Chiave e Componenti Verificate
Lo sviluppo Lean generato non ha prodotto una dimostrazione completa del teorema principale. Invece, ha dato luogo a un artefatto ibrido costituito da quattro lemmi ausiliari completamente verificati e un teorema principale irrisolto:

1. Componenti Locali Verificate:

   • PS last: Verificato che la somma parziale finale sia uguale alla somma totale dei salti.
   • PS swap: Verificato che una trasposizione adiacente dei salti influenzi solo la specifica somma parziale intermedia in quella posizione, lasciando invariate tutte le altre.
   • PS swap eq: Verificata la forma algebrica della somma parziale modificata dopo uno scambio ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$).
   • maximizer swap in M: Verificato un argomento di massimalità locale. Stabilisce che se una permutazione massimizza una specifica funzione di punteggio $G(\sigma)$, e una somma parziale in una posizione scambiabile è in $M$, allora il valore risultante dallo scambio deve essere anch'esso in $M$.

2. Componente Globale Irrisolta:

   • Il teorema principale, grasshopper, è chiuso direttamente da un singolo sorry.
   • Il riepilogo dell'output di Aristotle identifica il passaggio mancante come un argomento di conteggio globale. Mentre i lemmi locali stabiliscono che scambi specifici costringono l'appartenenza a $M$, il sistema non è riuscito a coordinare questi fatti per dimostrare che generano almeno $n$ valori proibiti distinti, il che contraddirebbe l'assunzione $|M| < n$. Il codice sorgente Lean non riduce il teorema principale a un lemma di conteggio separato e codificato; il divario rimane un obbligo non dimostrato.

Contributi
L'articolo apporta due contributi principali:

1. Un Artefatto Riproducibile: Fornisce un tentativo di formalizzazione in Lean 4 ispezionabile e riproducibile di un difficile problema di combinatoria olimpica utilizzando l'API Aristotle, includendo il codice sorgente completo e i log di esecuzione.
2. Un'Analisi Precisa dei Limiti dell'IA: Offre una dissezione dettagliata dello "status probatorio" delle dimostrazioni generate dall'IA. Lo studio dimostra che i sistemi di IA possono verificare con successo passaggi locali, algebrici e basati su scambi, fallendo tuttavia nell'eseguire la contabilità combinatoria globale necessaria per chiudere il teorema principale.

Significato e Affermazioni
L'articolo sostiene che la distinzione tra "dichiarazioni verificate" e "dichiarazioni chiuse da sorry" è critica per l'interpretazione della dimostrazione di teoremi assistita dall'IA. Il significato di questo studio di caso risiede nella sua dimostrazione che la ricerca di prove locali può avere successo mentre il ragionamento globale rimane irrisolto.

Gli autori sottolineano che una compilazione riuscita di un file Lean contenente sorry è una prova insufficiente di una dimostrazione completata. L'artefatto funge da esempio cautelativo: mentre gli strumenti di IA possono generare sviluppi matematici sostanziali e verificati (come i quattro lemmi ausiliari), possono comunque lasciare il motore logico centrale della dimostrazione (la contraddizione globale) non implementato. L'articolo conclude che una formalizzazione assistita dall'IA affidabile richiede un'ispezione rigorosa degli obblighi e delle dipendenze di prova, piuttosto che un affidamento sulla mera presenza di codice generato.