AI RESEARCH
Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
arXiv CS.AI
•
ArXi:2605.20120v1 Announce Type: new 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 formalization of an Aristotle API proof attempt for the Grasshopper problem, originally posed as IMO 2009 Problem 6.