LeanTutor: Towards a Verified AI Mathematical Proof Tutor

Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss +2 more
1/24/2026
cs.LG

No confident code implementation found for this paper.

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4

90% match2024

Autograding Mathematical Induction Proofs with Natural Language Processing

86% match2024

Formal Mathematical Reasoning: A New Frontier in AI

86% match2024

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

85% match1 repo752025

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

85% match1 repo272025

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean

85% match1 repo1.3k2024

Cite this paper

@article{patel2026leantutor,
  title  = {LeanTutor: Towards a Verified AI Mathematical Proof Tutor},
  author = {Manooshree Patel and Rayna Bhattacharyya and Thomas Lu and Arnav Mehta and Niels Voss and Narges Norouzi and Gireeja Ranade},
  year   = {2026},
  eprint = {2601.17473},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2601.17473v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2601.17473.svg)](https://codeofpaper.com/paper/2601.17473)

Discussion