# LeanTutor: Towards a Verified AI Mathematical Proof Tutor

arXiv: https://arxiv.org/abs/2506.08321 · HTML: https://mlsanity.com/paper/2506.08321/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 71 references that are in the map.
- First posted on arXiv 10 Jun 2025.

## Builds on (most cited first, 27 of 27)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Scaling Synthetic Data Creation with 1,000,000,000 Personas](https://mlsanity.com/paper/2406.20094/) (2024)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [SPoC: Search-based Pseudocode to Code](https://mlsanity.com/paper/1906.04908/) (2019)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Neural Machine Translation for Low-Resource Languages: A Survey](https://mlsanity.com/paper/2106.15115/) (2021)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [Unifying AI Tutor Evaluation: An Evaluation Taxonomy for Pedagogical Ability Assessment of LLM-Powered AI Tutors](https://mlsanity.com/paper/2412.09416/) (2024)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Tutor CoPilot: A Human-AI Approach for Scaling Real-Time Expertise](https://mlsanity.com/paper/2410.03017/) (2024)
- [Learning gain differences between ChatGPT and human tutor generated algebra hints](https://mlsanity.com/paper/2302.06871/) (2023)
- [MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data](https://mlsanity.com/paper/2402.08957/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [MathConstruct: Challenging LLM Reasoning with Constructive Proofs](https://mlsanity.com/paper/2502.10197/) (2025)
- [Automatic Generation of Question Hints for Mathematics Problems using Large Language Models in Educational Technology](https://mlsanity.com/paper/2411.03495/) (2024)
- [Live Functional Programming with Typed Holes](https://mlsanity.com/paper/1805.00155/) (2018)
- [HintEval: An Open-Source Python Toolkit for Hint Generation and Hint Evaluation](https://mlsanity.com/paper/2502.00857/) (2025)
- [ProofBuddy: A Proof Assistant for Learning and Monitoring](https://mlsanity.com/paper/2308.06970/) (2023)
- [Teaching Divisibility and Binomials with Coq](https://mlsanity.com/paper/2404.12676/) (2024)
- [Maths with Coq in L1, a pedagogical experiment](https://mlsanity.com/paper/2505.05990/) (2025)

## Built on by (most cited first, 4 of 4)

- [Retrieval-Augmented Tutoring for Algorithm Tracing and Problem-Solving in AI Education](https://mlsanity.com/paper/2605.12988/) (2026)
- [Reasoning Trajectories for Socratic Debugging of Student Code: From Misconceptions to Contradictions and Updated Beliefs](https://mlsanity.com/paper/2511.00371/) (2025)
- [Correct Diagnosis, Better Feedback: A Symbolic-Verifier for Faithful LLM Tutoring Feedback in Logic Proofs](https://mlsanity.com/paper/2609.22553/) (2026)
- [LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification](https://mlsanity.com/paper/2610.17697/) (2026)

## Abstract (arXiv)

This paper considers the development of an AI-based provably-correct mathematical proof tutor. While Large Language Models (LLMs) allow seamless communication in natural language, they are error prone. Theorem provers such as Lean allow for provable-correctness, but these are hard for students to learn. We present a proof-of-concept system (LeanTutor) by combining the complementary strengths of LLMs and theorem provers. LeanTutor is composed of three modules: (i) an autoformalizer/proof-checker, (ii) a next-step generator, and (iii) a natural language feedback generator. To evaluate the system, we introduce PeanoBench, a dataset of 371 Peano Arithmetic proofs in human-written natural language and formal language, derived from the Natural Numbers Game.