Reproduce “LeanTutor: Towards a Verified AI Mathematical Proof Tutor” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade
LeanTutor translates student natural-language proof steps into Lean tactics, checks them with the Lean compiler, and uses remaining proof states to generate feedback. On 21 selected incorrect proofs successfully autoformalized, human ratings for next-step feedback exceeded a baseline in accuracy, 3.7 versus 2.8, and relevance, 3.9 versus 2.9. This proof of concept does not measure learning or verify student reasoning.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.