LeanTutor: Towards a Verified AI Mathematical Proof Tutor - Patel, Manooshree; Bhattacharyya, Rayna; Lu, Thomas; Mehta, Arnav; Voss, Niels; Norouzi, Narges; Ranade, Gireeja (Proceedings of the AAAI Conference on Artificial Intelligence, 2026)
This paper considers the development of an AI-basedprovably-correct mathematical proof tutor. While LargeLanguage Models (LLMs) allow seamless communication innatural language, they are error prone. Theorem proverssuch as Lean allow for provable-correctness, but these arehard for students to learn. We present a proof-of-conceptsystem (LeanTutor) by combining the complementary strengthsof LLMs and theorem provers. LeanTutor is composed of threemodules: (i) an autoformalizer/proof-checker, (ii) anext-step generator, and (iii) a natural language feedbackgenerator. To evaluate the system, we introduce PeanoBench,a dataset of 371 Peano Arithmetic proofs in human-writtennatural language and formal language, derived from theNatural Numbers Game.