Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
The article discusses a case study on using the Aristotle API for AI-assisted theorem proving in Lean 4, focusing on the Grasshopper problem. It highlights the limitations of local proof search in AI-assisted formalization, where local components may be verified while the overall theorem remains unresolved. The study provides a reproducible Lean artifact and a detailed analysis of verified and unverified proof content.
- ▪The paper presents a formalization case study of the Grasshopper problem using the Aristotle API in Lean 4.
- ▪It identifies a limitation in AI-assisted theorem proving, where local proofs can succeed while global combinatorial aspects remain unresolved.
- ▪The study includes a Lean artifact that demonstrates both verified and unverified components of the proof.
Opening excerpt (first ~120 words) tap to expand
Computer Science > Artificial Intelligence arXiv:2605.20120 (cs) [Submitted on 19 May 2026] Title:Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem Authors:Gabriel Rongyang Lau View a PDF of the paper titled Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem, by Gabriel Rongyang Lau View PDF HTML (experimental) 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.
…
Excerpt limited to ~120 words for fair-use compliance. The full article is at arXiv cs.AI.
Discussion
0 commentsMore from arXiv cs.AI
