TY  - RPRT
TI  - Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
AU  - Gabriel Rongyang Lau
PY  - 2026
UR  - https://arxiv.org/abs/2605.20120
ID  - 2605.20120
ER  -