mlsanityData to 14 Oct 2026

LeanTutor: Towards a Verified AI Mathematical Proof Tutor

arXiv 2601.17473 ↗First posted 24 Jan 2026cs.LGcited by 0

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. No citing papers in the map yet (data through 14 Oct 2026). Builds on 27 of its 71 references that are in the map. First posted on arXiv 24 Jan 2026.

Builds on

27 of 71 references.

References · 27

  1. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 9,379
  2. 2024Scaling Synthetic Data Creation with 1,000,000,000 Personascited by 417
  3. 2023Llemma: An Open Language Model For Mathematicscited by 388
  4. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  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 122
  7. 2021Neural Machine Translation for Low-Resource Languages: A Surveycited by 109
  8. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 82
  9. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  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 61
  12. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 59
15 more
  1. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 59
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  3. 2024Tutor CoPilot: A Human-AI Approach for Scaling Real-Time Expertisecited by 50
  4. 2023Learning gain differences between ChatGPT and human tutor generated algebra hintscited by 43
  5. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  6. 2024Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistencycited by 41
  7. 2019Generating Correctness Proofs with Neural Networkscited by 37
  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

Not cited yet.