LeanTutor: Towards a Verified AI Mathematical Proof Tutor

2025/06/10 by Manooshree Patel, Patel, Manooshree, Bhattacharyya, Rayna +9 · 1 citation
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Human-Computer Interaction (cs.HC) #Intelligent Tutoring Systems and Adaptive Learning #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Mathematics, Computing, and Information Processing

paper · pdf · doi:10.48550/arxiv.2506.08321

openalex publication_date 2025/06/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30

Abstract

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.

Citations

• MathConstruct: Challenging LLM Reasoning with Constructive Proofs
• HintEval: A Comprehensive Framework for Hint Generation and Evaluation for Questions
• Formal Mathematical Reasoning: A New Frontier in AI
• Automatic Generation of Question Hints for Mathematics Problems using Large Language Models in Educational Technology
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
• Herald: A Natural Language Annotated Lean 4 Dataset
• Tutor CoPilot: A Human-AI Approach for Scaling Real-Time Expertise
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
• Scaling Synthetic Data Creation with 1,000,000,000 Personas
• Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
• Teaching Divisibility and Binomials with Coq
• A Survey on Deep Learning for Theorem Proving
• BioXP-0.5B: Explainable Medical-AI via RL-GRPO
• Llemma: An Open Language Model For Mathematics
• An In-Context Learning Agent for Formal Theorem-Proving
• Learning gain differences between ChatGPT and human tutor generated algebra hints
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
• NaturalProver: Grounded Mathematical Proof Generation with Language Models
• Neural Machine Translation for Low-Resource Languages: A Survey
• Generating Correctness Proofs with Neural Networks
• SPoC: Search-based Pseudocode to Code
• Live Functional Programming with Typed Holes
• Automated Feedback Generation for Introductory Programming Assignments

Cited by

• Reasoning Trajectories for Socratic Debugging of Student Code: From Misconceptions to Contradictions and Updated Beliefs

Related

• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
• Autograding Mathematical Induction Proofs with Natural Language Processing
• IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data