Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
DGX agentarXiv:2605.20120v1 Announce Type: new Abstract: AI-assisted theorem proving can now generate substantial Lean developments for olympiad-level mathematics, but the evidential status of such development