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

Technical Summary: A Formalisation Case Study of the Grasshopper Problem Using the Aristotle API

Problem Statement
This paper presents a formalisation case study of the "Grasshopper problem," originally posed as Problem 6 of the 50th International Mathematical Olympiad (IMO 2009). The theorem states that for any set of $n$ distinct positive integers $\{a_1, \dots, a_n\}$ and a set $M$ of $n-1$ positive integers (where the total sum $\sum a_i \notin M$), there exists a permutation $\sigma$ of the jumps such that no intermediate partial sum $S_k = \sum_{i=1}^k a_{\sigma(i)}$ lands in $M$. The problem is noted for its historical difficulty, having the lowest mean score among all 2009 IMO problems, and requires non-trivial combinatorial reasoning involving permutations and forbidden sets.

Methodology
The study utilizes the Aristotle API, an automated theorem-proving system that combines language-model-guided search, informal lemma generation, and formalisation within the Lean 4 proof assistant (using Mathlib). The authors provided a specific prompt to the Aristotle API requesting a rigorous, complete proof of the Grasshopper problem, explicitly forbidding citations of the problem as a known theorem and demanding the construction of a valid permutation.

The resulting artefact is a Lean 4 project containing a generalised version of the theorem (allowing $|M| < n$ rather than strictly $n-1$, and permitting $0 \in M$). The authors performed a granular inspection of the generated code to distinguish between declarations that are fully machine-verified and those containing unresolved proof placeholders (sorry).

Key Results and Verified Components
The generated Lean development did not produce a complete proof of the main theorem. Instead, it resulted in a hybrid artefact consisting of four fully verified helper lemmas and one unresolved main theorem:

1. Verified Local Components:

   • PS last: Verified that the final partial sum equals the total sum of the jumps.
   • PS swap: Verified that an adjacent transposition of jumps affects only the specific intermediate partial sum at that position, leaving all others unchanged.
   • PS swap eq: Verified the algebraic form of the changed partial sum after a swap ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$).
   • maximizer swap in M: Verified a local maximality argument. It establishes that if a permutation maximizes a specific score function $G(\sigma)$, and a partial sum at a swappable position is in $M$, then the value resulting from the swap must also be in $M$.

2. Unresolved Global Component:

   • The main theorem, grasshopper, is closed directly by a single sorry.
   • The Aristotle output summary identifies the missing step as a global counting argument. While the local lemmas establish that specific swaps force membership in $M$, the system failed to coordinate these facts to prove that they generate at least $n$ distinct forbidden values, which would contradict the assumption $|M| < n$. The Lean source does not reduce the main theorem to a separate, encoded counting lemma; the gap remains an unproved obligation.

Contributions
The paper makes two primary contributions:

1. A Reproducible Artefact: It provides an inspectable, reproducible Lean 4 formalisation attempt of a difficult olympiad combinatorics problem using the Aristotle API, including the full source code and run logs.
2. A Precise Analysis of AI Limitations: It offers a detailed dissection of the "evidential status" of AI-generated proofs. The study demonstrates that AI systems can successfully verify local, algebraic, and exchange-based reasoning steps while failing to execute the global combinatorial bookkeeping required to close the main theorem.

Significance and Claims
The paper argues that the distinction between "verified declarations" and "declarations closed by sorry" is critical for the interpretation of AI-assisted theorem proving. The significance of this case study lies in its demonstration that local proof search can succeed while global reasoning remains unresolved.

The authors emphasize that a successful compilation of a Lean file containing sorry is insufficient evidence of a completed proof. The artefact serves as a cautionary example: while AI tools can generate substantial, verified mathematical developments (such as the four helper lemmas), they may still leave the core logical engine of the proof (the global contradiction) unimplemented. The paper concludes that trustworthy AI-assisted formalisation requires rigorous inspection of proof obligations and dependencies, rather than reliance on the mere presence of generated code.