mlsanityData to 7 Oct 2026

LeanTutor: Towards a Verified AI Mathematical Proof Tutor

arXiv 2506.08321 ↗First posted 10 Jun 2025cs.AI cs.HC cs.LOcited by 3

Not on the map. Why?

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.

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

Builds on

27 of 71 references.

References · 27

  1. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  2. 2024Scaling Synthetic Data Creation with 1,000,000,000 Personascited by 397
  3. 2023Llemma: An Open Language Model For Mathematicscited by 385
  4. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  5. 2019SPoC: Search-based Pseudocode to Codecited by 176
  6. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  7. 2021Neural Machine Translation for Low-Resource Languages: A Surveycited by 108
  8. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  9. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  10. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  11. 2024Unifying AI Tutor Evaluation: An Evaluation Taxonomy for Pedagogical Ability Assessment of LLM-Powered AI Tutorscited by 60
  12. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
15 more
  1. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  2. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 54
  3. 2024Tutor CoPilot: A Human-AI Approach for Scaling Real-Time Expertisecited by 46
  4. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  5. 2023Learning gain differences between ChatGPT and human tutor generated algebra hintscited by 42
  6. 2024Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistencycited by 39
  7. 2019Generating Correctness Proofs with Neural Networkscited by 36
  8. 2023Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofscited by 27
  9. 2025MathConstruct: Challenging LLM Reasoning with Constructive Proofscited by 16
  10. 2024Automatic Generation of Question Hints for Mathematics Problems using Large Language Models in Educational Technologycited by 9
  11. 2018Live Functional Programming with Typed Holescited by 7
  12. 2025HintEval: An Open-Source Python Toolkit for Hint Generation and Hint Evaluationcited by 3
  13. 2023ProofBuddy: A Proof Assistant for Learning and Monitoringcited by 2
  14. 2024Teaching Divisibility and Binomials with Coqcited by 2
  15. 2025Maths with Coq in L1, a pedagogical experimentcited by 2

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 1; 2026: 2.

3 papers.

  1. 2025Reasoning Trajectories for Socratic Debugging of Student Code: From Misconceptions to Contradictions and Updated Beliefscited by 0
  2. 2026Retrieval-Augmented Tutoring for Algorithm Tracing and Problem-Solving in AI Educationcited by 0
  3. 2026Correct Diagnosis, Better Feedback: A Symbolic-Verifier for Faithful LLM Tutoring Feedback in Logic Proofscited by 0