USING THE ARISTOTLE API FOR AI-ASSISTED THEOREM PROVING IN LEAN 4: A FORMALISATION CASE STUDY OF THE GRASSHOPPER PROBLEM GABRIEL R. LAU
arXiv:2605.20120v1 [cs.AI] 19 May 2026
Nanyang Technological University, Singapore [email protected] Abstract. AI-assisted theorem proving can now generate substantial Lean developments for olympiad-level mathematics, but the evidential status of such developments depends on which declarations are actually verified. This paper reports a Lean 4 formalisation case study of an Aristotle API proof attempt for the Grasshopper problem, originally posed as IMO 2009 Problem 6. The generated artefact states a generalised Lean version of the theorem, contains four verified helper lemmas for local components of a maximality and adjacent-swap exchange strategy, and leaves the main theorem grasshopper closed directly by one unresolved sorry. The verified components establish that the final partial sum equals the total sum, that an adjacent transposition can affect only the relevant intermediate partial sum, that the changed partial sum has the expected form, and that maximality at a position admitting an adjacent successor swap forces a corresponding forbidden-set membership fact. The Aristotle output summary identifies the intended remaining mathematical step as the global counting step needed to show that these membership facts produce at least n distinct forbidden values, contradicting the cardinality assumption |M | < n; the Lean source itself does not reduce the main theorem to a separately encoded counting lemma. This case study gives an inspectable example of a central limitation in AI-assisted formalisation, namely that local proof search can succeed while the global combinatorial bookkeeping required for a theorem remains unresolved. The paper contributes a reproducible Lean artefact and a precise analysis of its verified and unverified proof content.
1. Introduction AI-assisted theorem proving raises a practical problem of proof interpretation. When an AI system generates a Lean development, one must distinguish between declarations that are fully verified and declarations that are accepted only because they contain unresolved proof placeholders. Since Lean accepts declarations closed by sorry, successful compilation alone is insufficient evidence of a completed proof. In Lean, sorry is a placeholder that allows a declaration to be accepted without a completed proof. A theorem closed by sorry should therefore not be treated as a machine-checked proof [8]. This paper examines that distinction through a Lean 4 formalisation attempt for the Grasshopper problem, originally posed as IMO 2009 Problem 6. The Grasshopper problem was posed as Problem 6 of the 50th International Mathematical Olympiad, held in Bremen, Germany, in July 2009. The official IMO individual-results table records contestant-level scores for all six problems. Aggregating the Problem 6 scores shows that it was the least solved problem of the competition, with mean score 0.168 out of 7 and 540 contestants receiving zero points [5]. Contemporary discussion by Tao treated the problem as a suitable subject for collaborative exploration [7]. Related work of Kós studies a signedjump variant and contrasts the original problem with variants for which polynomial-method arguments become available [6]. Date: May 2026. 2020 Mathematics Subject Classification. Primary 68V20; Secondary 03B35, 05A05. Key words and phrases. AI-assisted theorem proving, automated theorem proving, proof assistants, Lean 4, formal verification, olympiad mathematics, AI for mathematics.
1
2
GABRIEL R. LAU
This case study is situated within recent work combining language-model-guided search with formal proof assistants. The miniF2F benchmark was introduced to evaluate formal olympiadlevel mathematics across proof-assistant systems [12]. DeepSeek-Prover uses large-scale synthetic Lean data to improve theorem proving by language models [11]. AlphaGeometry combines neural guidance with symbolic deduction for olympiad geometry problems [10]. Aristotle is described in its technical report as an automated theorem-proving system using Lean proof search, informal lemma generation and formalisation, reinforcement-learning improvements, and a separate geometry solver [1]. The present paper studies a narrower artefact, a partial Aristotle-generated Lean 4 proof development for one combinatorial problem. The paper makes two contributions. First, it reports a case study of AI-assisted theorem proving in Lean 4 using the Aristotle API on a difficult olympiad combinatorics problem. Second, it illustrates a current limitation of AI-assisted formalisation, namely the gap between locally verified proof components and the broader mathematical reasoning needed to complete a proof. The case study interprets the generated Lean development by its verified declarations, dependencies, and unresolved proof obligations. 2. The Grasshopper Problem as a Formalisation Target We first state the mathematical theorem in its standard form. Theorem 1 (Grasshopper problem). Let n be a positive integer. Let a1 , . . . , an be distinct positive integers, and let M be a set of n − 1 positive integers such that a1 + · · · + an ∈ / M. Then there exists a permutation σ of {1, . . . , n} such that aσ(1) + · · · + aσ(k) ∈ /M for every 1 ≤ k ≤ n. Remark 2. Theorem 1 is stated to identify the mathematical target of the formalisation attempt. The present paper does not give a new proof of this theorem, and the accompanying Lean artefact does not contain a completed proof of it. The final condition at k = n is guaranteed by the hypothesis on the total sum, since the endpoint is independent of the ordering. The difficulty is to choose an ordering for which the first n − 1 partial sums avoid M . The positivity of the jumps ensures that landing positions move strictly to the right, while distinctness prevents certain exchange operations from becoming degenerate. The Lean statement generated in the reported artefact slightly generalises the original IMO formulation in two ways. First, its Lean cardinality hypothesis corresponds to |M | < n, rather than |M | = n − 1. This is a more general theorem statement, since it allows any forbidden set of cardinality less than n. Second, it uses M : Finset Nat, so zero may belong to M . This does not affect the original problem, because all landing positions after at least one jump are positive under the hypothesis 0 < ai . Although the informal problem assumes n > 0, the Lean statement allows n = 0. In that case the cardinality hypothesis |M | < n is impossible, so the theorem is vacuous. 3. Exchange Proof Strategy For a permutation σ, define the partial sums Sk (σ) = aσ(1) + · · · + aσ(k) ,
1 ≤ k ≤ n.
Call an index k safe for σ if Sk (σ) ∈ / M , and unsafe if Sk (σ) ∈ M . The Lean development defines a score G(σ) as the sum of the non-forbidden partial sums and proves a local exchange lemma conditional on a permutation σ satisfying a maximality hypothesis for this score. Under this maximality hypothesis, if the permutation has an unsafe index, one swaps adjacent jumps whose order affects the corresponding intermediate partial sum and compares the resulting partial sums.
AI-ASSISTED THEOREM PROVING
3
The local calculation is straightforward. Suppose two neighbouring jumps x and y occur after a previous partial sum P . Before the swap the intermediate landing is P + x, and after the swap it is P + y. All other relevant partial sums are unchanged. If the original ordering was chosen to maximise G, then a swap that increases the contribution at the changed partial sum while leaving the other contributions unchanged contradicts maximality. Thus maximality can force additional values of the form P + y to lie in M . The unresolved mathematical difficulty identified by the Aristotle output summary is the final counting argument. Completing the argument would require organising the values produced by many possible swaps and proving that they yield sufficiently many distinct elements of M to contradict |M | < n. A naive induction also runs into a size problem: removing one jump need not reduce the forbidden set from size n − 1 to size n − 2. In the Lean source itself, however, the main theorem is closed directly by sorry; the file does not formally reduce the theorem to a separately encoded global counting lemma. 4. AI-Assisted Lean Formalisation The formalisation attempt was conducted using the Aristotle API with Lean 4 and Mathlib [4, 9]. Aristotle is presented by Harmonic as a formal reasoning agent that can work from English mathematical input or inside an existing Lean project [2]. The public SDK documentation describes an API and command-line workflow for interacting with Lean files [3]. Listing 1 is a readability-oriented transcription of the theorem declaration. The accompanying Lean source remains authoritative for exact syntax, imports, notation, and proof status. In the listing, notin is used only as an ASCII rendering of Lean’s non-membership notation ∈. / Listing 1. ASCII-rendered transcription of the Aristotle-reported Lean theorem declaration theorem grasshopper (n : Nat) (a : Fin n -> Nat) (M : Finset Nat) (ha_pos : forall i, 0 < a i) (ha_inj : Injective a) (hM_card : M.card < n) (hS : (sum i, a i) notin M) : exists sigma : Equiv.Perm (Fin n), forall k : Fin n, PS a sigma k notin M := by sorry
The use of Fin n represents jump indices as a finite type. A permutation of jumps is represented by Equiv.Perm (Fin n). The helper definition PS represents partial sums over initial segments such as Finset.Iic k. This encoding is standard in Lean, but it requires explicit lemmas connecting final partial sums, adjacent swaps, and finite-set sums. The finite type Fin n is zero-indexed. Thus the formal index k : Fin n indexes a landing position in the ordered sequence; it is not a literal rendering of the informal index 1 ≤ k ≤ n. When n > 0, the first element of Fin n corresponds to the first landing position, and the last element corresponds to the final landing position. 5. Verified Local Proof Components Table 1 summarises the verification status reported for the Aristotle-generated Lean development.
4
GABRIEL R. LAU
Lean component
Mathematical role
Status
Final partial sum equals total sum Verified Adjacent transposition can affect Verified only one relevant intermediate partial sum PS swap eq Computes the changed partial sum Verified after an adjacent swap maximizer swap in M Converts maximality into a Verified forbidden-set membership fact grasshopper Main theorem Incomplete, one sorry Table 1. Verification status of the Aristotle-generated Lean development. PS last PS swap
The verified helper lemmas correspond to the local portion of the exchange proof. The lemma PS last establishes that the final formal partial sum agrees with the total sum. The lemmas PS swap and PS swap eq formalise the effect of an adjacent transposition: such a swap can affect only the relevant intermediate partial sum, and the changed partial sum has the expected value. The lemma maximizer swap in M formalises a maximality argument. If a chosen permutation maximises G and the partial sum at a position admitting an adjacent successor swap is forbidden, then the value obtained by that adjacent swap must also be forbidden. These lemmas verify the local exchange calculations needed to track partial sums under adjacent transpositions. They formalise the part of the exchange argument where the informal proof relies on the claim that adjacent swaps preserve all partial sums except the relevant intermediate one. They do not imply the Grasshopper theorem. 6. The Intended Global Counting Argument The Aristotle output summary identifies the intended remaining mathematical step as the final counting or contradiction argument. Informally, the verified maximality lemma produces new membership facts in M at positions admitting adjacent successor swaps. To finish the theorem, one would have to show that these facts force at least n distinct forbidden values, contradicting |M | < n. This step is global. It must track possible collisions among values obtained from different swaps, use injectivity of the jump-length function, and relate the resulting set of values to the finite-cardinality assumption. In the Lean source itself, however, the main theorem grasshopper is closed directly by sorry. Thus, the artefact should be read as four verified helper lemmas together with an unproved main theorem, rather than as a formal Lean proof reduced to a separately encoded counting lemma. 7. Reproducibility and Artefact Inspection The accompanying Lean archive contains the following project files and supporting documentation. • ARISTOTLE SUMMARY.md • README.md • figures/aristotle-run-provenance.png • RequestProject/Grasshopper.lean • RequestProject/Main.lean • lean-toolchain • lakefile.toml • lake-manifest.json. The visible Aristotle run log indicates an approximate runtime of eight hours. Figure 1 shows the visible run-log evidence for this approximate runtime.
AI-ASSISTED THEOREM PROVING
5
Figure 1. Aristotle run log for the reported partial formalisation attempt. 8. Implications for AI-Assisted Theorem Proving The case study separates two kinds of formalisation work. Aristotle successfully handled local reasoning involving finite sums, permutations, adjacent swaps, and a maximality lemma. These tasks are amenable to proof-assistant verification once the relevant definitions are in place. The generated development did not prove the main theorem. The Aristotle output summary identifies the intended missing mathematical step as the global counting or contradiction argument, which would require coordinating maximality, injectivity, positivity, and finite-cardinality estimates across many candidate partial sums. The Lean source itself does not encode this as a separate final subgoal; it closes grasshopper directly by sorry. Accordingly, the missing argument should be treated as an unproved obligation, not as a completed machine-checked argument. For AI-assisted theorem proving, the lesson is methodological. A formal artefact should be inspected at the level of declarations, dependencies, placeholders, and proof obligations. This distinction matters for trustworthy AI because generated proof attempts may combine verified components with unresolved obligations. The artefact is useful as a case study because its verification status is inspectable. It contains verified local components and a clearly identified missing proof obligation.
6
GABRIEL R. LAU
Code availability The supplementary archive grasshopper-lean-artifact.zip, provided with this paper as supplementary material in the arXiv source package, contains the Lean project. To inspect the artefact, unzip the archive and run lake build from the project root. The main theorem grasshopper remains closed by sorry; the helper lemmas listed in Table 1 were inspected separately. Appendix A. Prompt Given to Aristotle API Solve the following extremely difficult IMO-level combinatorics problem rigorously. Let n be a positive integer. Let a_1, a_2, ..., a_n be distinct positive integers, and let M be a set of n - 1 positive integers such that a_1 + a_2 + ... + a_n is not in M. A grasshopper starts at position 0 on the number line. It will make n jumps to the right, using the jump lengths a_1, a_2, ..., a_n in some order, each exactly once. Prove that there exists an ordering of the jumps such that the grasshopper never lands on any point in M. Requirements: 1. Give a complete proof, not just a sketch. 2. Do not cite this as a known theorem or IMO problem. 3. Prove all auxiliary lemmas used. 4. The proof must work for all positive integers n. 5. The argument must explicitly construct or justify the existence of a valid permutation of the jump lengths. 6. Avoid computational checking except for trivial base cases. 7. If using induction, carefully justify the reduction step, especially how the forbidden set changes. 8. If using a maximality, exchange, or graph-theoretic argument, clearly define the object being optimised and prove why the chosen object must satisfy the required avoidance property.
Appendix B. Aristotle Output Summary This appendix records the final Aristotle output summary for provenance. The mathematical interpretation of these claims is given in Sections 4 to 7. Grasshopper Problem, partial formalisation. Aristotle reported that it formalised the Grasshopper problem in RequestProject/Grasshopper.lean. The reported theorem declaration can be rendered schematically in ASCII as follows. theorem grasshopper (n : Nat) (a : Fin n -> Nat) (M : Finset Nat) (ha_pos : forall i, 0 < a i) (ha_inj : Injective a) (hM_card : M.card < n) (hS : (sum i, a i) notin M) : exists sigma : Equiv.Perm (Fin n), forall k : Fin n, PS a sigma k notin M := by sorry
Aristotle reported four helper lemmas as fully verified. P ai . • PS last. The final partial sum Sn (σ) equals the total sum
AI-ASSISTED THEOREM PROVING
7
• PS swap. An adjacent transposition of positions k and k + 1 can affect only the intermediate partial sum Sk (σ); all other partial sums Sj (σ) are unchanged. • PS swap eq. The partial sum at position k after an adjacent swap equals Sk (σ) − aσ(k) + aσ(k+1) . • maximizer swap in M. For a permutation satisfying the G-maximality hypothesis, if the partial sum Sk (σ) at a position with an adjacent successor swap is in M , then the swapped value Sk (σ) − aσ(k) + aσ(k+1) is also in M . The main theorem grasshopper is closed directly by one sorry. The Aristotle output summary identifies the intended remaining mathematical step as the final counting or contradiction argument, where one would show that the constraints from maximizer swap in M force |M | ≥ n, contradicting |M | < n. References [1] Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathı̈s Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, and Lawrence Wu. Aristotle: IMO-level automated theorem proving. arXiv preprint arXiv:2510.01346, 2025. doi:10.48550/arXiv.2510.01346. [2] Aristotle API. https://aristotle.harmonic.fun/. Accessed 2026-05-19. [3] aristotlelib. Python library and command-line tool for the Aristotle API. https://pypi.org/project/ aristotlelib/. Accessed 2026-05-19. [4] Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction – CADE 28, volume 12699 of Lecture Notes in Computer Science, pages 625–635, Cham, 2021. Springer. doi:10.1007/978-3-030-79876-5_37. [5] 50th International Mathematical Olympiad 2009. Individual results. https://www.imo-official.org/resu lts/individual/year/2009/. Accessed 2026-05-19. [6] Géza Kós. On the grasshopper problem with signed jumps. The American Mathematical Monthly, 118(10):877–886, 2011. doi:10.4169/amer.math.monthly.118.10.877. [7] Terence Tao. IMO 2009 Q6 as a mini-polymath project. https://terrytao.wordpress.com/2009/07/20/ imo-2009-q6-as-a-mini-polymath-project/, 2009. Accessed 2026-05-19. [8] The Lean Language Reference. Tactic Reference, section on the sorry tactic. https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/. Accessed 202605-19. [9] The mathlib Community. Mathlib4: The Lean Mathematical Library. https://github.com/ leanprover-community/mathlib4. Software project. Accessed 2026-05-19. [10] Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625:476–482, 2024. doi:10.1038/s41586-023-06747-5. [11] Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024. doi:10.48550/arXiv.2405.14333. [12] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022. doi:10.48550/arXiv.2109.00110.