Formal Verification

LeanTutor: Towards a Verified AI Mathematical Proof Tutor

Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade

Proceedings of the AAAI Conference on Artificial Intelligence

LeanTutor connects a language model to the Lean theorem prover to support mathematical proof feedback. Its technical evaluation shows promising hints on a small selected benchmark, but also exposes a crucial boundary: a verifier can check the formal proof only after the learner's words have been translated correctly. The study did not test classroom learning, and feedback evaluation excluded failed translations. It is an early system design with explicit limitations, not a validated replacement for mathematics instruction.