LeanTutor: Towards a Verified AI Mathematical Proof Tutor

This paper introduces LeanTutor, a proof-of-concept system that combines Large Language Models with theorem provers to create an AI mathematical proof tutor, and evaluates its effectiveness using the newly introduced PeanoBench dataset.

The Gist

Imagine you are learning to play a complex instrument, like the violin. You have two potential teachers:

1. The "Genius" AI (LLM): This teacher is incredibly chatty, speaks your language perfectly, and can write beautiful music. But, they are prone to making up facts. They might tell you, "Just press this string here," and when you do, it sounds terrible. They are confident, but often wrong.
2. The "Robot" Musician (Theorem Prover): This teacher is a machine that never makes a mistake. If you play a wrong note, it immediately beeps and says, "Error." But, it speaks in a secret code (mathematical symbols) that is incredibly hard for a human to understand. It can't explain why you're wrong in a way that helps you learn; it just stops you.

LeanTutor is the dream collaboration between these two. It combines the friendly, conversational nature of the "Genius" AI with the unshakeable accuracy of the "Robot" Musician.

Here is how the paper breaks down this idea in simple terms:

The Problem: The "Helpful" Trap

Right now, students use AI chatbots (like ChatGPT) to help with math proofs. The problem is that these chatbots are designed to be helpful, which often means they just give you the answer. Worse, they sometimes "hallucinate"—they confidently explain a math concept that is completely made up. In a math class, getting a wrong answer with a confident explanation is dangerous because it stops you from learning how to think.

The Solution: LeanTutor

The researchers built a system called LeanTutor. Think of it as a three-person team working together to help a student:

1. The Translator (Autoformalizer):

   • What it does: The student types their proof in plain English (e.g., "I will start by assuming x is zero"). The Translator instantly converts this into the strict, secret code that the Robot Musician understands.
   • The Analogy: Imagine you are speaking English, and a translator instantly turns your words into a computer program. If you make a grammar mistake in English, the translator might get confused, but LeanTutor tries to be very careful to keep your meaning exactly the same.

2. The Referee (Next-Step Generator):

   • What it does: Once the Translator converts the student's idea into code, the Robot Musician checks it. If the student is stuck or made a mistake, the Referee looks at the "Game Board" (the current state of the proof) and suggests the next valid move.
   • The Analogy: Think of a chess coach. You make a move, and the coach says, "That's a legal move, but it doesn't get you closer to winning. Try moving your knight here instead." The coach knows the rules perfectly but doesn't just play the game for you.

3. The Coach (Feedback Generator):

   • What it does: The Referee knows the next move, but it speaks in code. The Coach takes that code and translates it back into friendly, natural English advice.
   • The Analogy: Instead of saying "Error: Syntax mismatch," the Coach says, "You're trying to skip a step! Remember, you need to prove the base case before you move to the next one. Try simplifying that first part."

The Training Ground: PeanoBench

To teach this system, the researchers couldn't just use random math problems. They needed a specific set of practice problems where they knew the answer perfectly. They created PeanoBench, a dataset of 371 math proofs about basic numbers (Peano Arithmetic).

• They took existing proofs from a game called "Natural Numbers Game."
• They created "Correct" versions (written by experts).
• They created "Incorrect" versions by intentionally removing steps or making logical jumps, mimicking the mistakes real students make.
• They wrote these in different "personalities" (some very short and algebraic, some very wordy and explanatory) to make the system robust.

How They Tested It

They didn't just hope it worked; they tested it rigorously.

• They gave the system incorrect proofs (the kind a student would write).
• They compared LeanTutor against a standard AI chatbot.
• The Result: LeanTutor was much better at spotting exactly where the student went wrong and giving a hint that guided them to the solution without just handing over the answer. The standard AI often gave vague advice or accidentally revealed the whole answer.

The Catch (Limitations)

The paper admits this is a "Proof of Concept" (a working prototype), not a finished product yet.

• The Translation Gap: If the student's English is too messy or vague, the Translator might get it wrong, and the whole system breaks.
• The "Perfect Answer" Requirement: Currently, the system needs a "Staff Solution" (a perfect proof written by a human) to work. It can't invent a new proof from scratch; it just guides you toward a known solution.
• Scope: Right now, it only works on basic number theory. It hasn't been tested on complex calculus or advanced physics yet.

The Big Picture

The ultimate goal of LeanTutor is to create a math tutor that is safe. It uses the AI to talk to you like a human, but it uses a "truth machine" (the theorem prover) in the background to ensure that every piece of advice is mathematically 100% correct. It's the best of both worlds: the patience of a human tutor with the precision of a supercomputer.

Technical Summary

Here is a detailed technical summary of the paper "LeanTutor: Towards a Verified AI Mathematical Proof Tutor."

1. Problem Statement

The paper addresses the limitations of using Large Language Models (LLMs) as educational tools for mathematical proofs. While LLMs offer natural language interaction, they suffer from:

• Hallucinations: Generating convincing but mathematically incorrect answers.
• Lack of Pedagogical Strategy: Often providing direct answers rather than guiding students through reasoning.
• Inability to Verify: Inability to guarantee the correctness of a proof or identify specific logical errors.

Conversely, formal theorem provers (like Lean) offer provable correctness but are hindered by:

• High Barrier to Entry: Complex syntax makes them difficult for students to learn.
• Rigidity: They often require strict input formats, lacking the flexibility of natural language.

The Goal: To develop a "proof-of-concept" tutoring system that combines the natural language fluency of LLMs with the rigorous verification capabilities of theorem provers to provide provably correct feedback without revealing the full solution.

2. Methodology: The LeanTutor System

LeanTutor is an architecture comprising three interconnected modules that bridge Natural Language (NL) and the Lean formal language (FL).

A. Core Modules

1. Autoformalizer & Proof Checker:

   • Function: Translates student NL proof steps into Lean tactics one-by-one.
   • Mechanism: It uses a general-purpose LLM (GPT-4o-mini) with in-context learning. The prompt includes the theorem statement, a dictionary of available tactics/theorems, 5-shot examples, and a Staff Solution (a reference proof in both NL and FL).
   • Verification: Each translated step is compiled using LeanInteract. If the compiler returns "unsolved goals," the step is accepted. If it returns a syntax or type error, the step is flagged as incorrect.
   • Strategy: It processes proofs step-by-step rather than generating the whole proof at once, allowing for immediate error detection.

2. Next Step Generator (NSG):

   • Function: When a student is stuck or makes an error, this module generates a valid next tactic to guide the student.
   • Mechanism: It performs an LLM-directed depth-first search. The LLM generates 12 candidate tactics. These are filtered by:
     • Compilation: Must compile in Lean.
     • Progress Check: Must not use forbidden theorems (e.g., the theorem being proved) and must not create cyclic proof states.
   • Search Space: The search is bounded (depth of 8) and limited to the specific "world" (topic) of the theorem to reduce complexity.

3. Natural Language Feedback Generator:

   • Function: Converts technical Lean errors and the next valid tactic into pedagogical NL feedback.
   • Output Types:
     1. Error Identification: Explains why the student's step failed.
     2. Hint/Question: A guiding question to prompt the student's own reasoning.
     3. Bottom-out Hint: An explicit suggestion of the next step (without giving the full proof).
   • Input: Student's autoformalized proof, Lean compiler error messages, and the output from the NSG.

B. Dataset: PeanoBench

To train and evaluate the system, the authors created PeanoBench, a dataset of 371 proofs derived from the Natural Numbers Game 4 (NNG4).

• Composition:
  • Staff Solutions: Reference proofs from NNG4.
  • Correct Proofs: 225 proofs generated using two "personas" (Equation-based and Justification-based) to simulate varied student writing styles.
  • Incorrect Proofs: 146 proofs generated by algorithmically skipping steps (simulating common logical errors like missing inductive steps).
• Structure: Each proof has a one-to-one correspondence between NL steps and Lean tactics, facilitating granular evaluation.

3. Key Contributions

1. Hybrid Architecture: A novel framework that offloads reasoning and verification to a theorem prover while maintaining a natural language interface via LLMs.
2. Faithful Autoformalization Metric: The authors propose a new metric to evaluate autoformalization accuracy that goes beyond simple string matching. It includes a state-matching phase where proof states are normalized (renaming variables) to check for syntactic identity, ensuring the generated tactic is semantically equivalent to the ground truth even if variable names differ.
3. Step-by-Step vs. Whole-Proof: The paper demonstrates that step-by-step autoformalization outperforms "whole-proof" generation, particularly in handling incorrect student inputs, as it allows for early error detection.
4. Reference Solution Utilization: The system leverages a known "Staff Solution" as context to improve the LLM's ability to map NL to FL, acknowledging that tutoring systems differ from open-ended theorem proving because the solution is known.

4. Experimental Results

The system was evaluated on 21 incorrect proofs (cold-start and error-containing) using human evaluators (graduate students) and an LLM-as-a-judge (GPT-4).

• Autoformalization Performance:

  • Baseline + Staff Solution achieved 56.8% accuracy on correct tactics and 30.1% on incorrect proofs (compared to ~33% and ~14% for the baseline without staff solutions).
  • Step-by-step generation significantly outperformed whole-proof generation on incorrect proofs (30.1% vs 21.9%).
  • Limitation: The model heavily relies on the Staff Solution; if the student's approach diverges significantly from the reference, accuracy drops.

• Feedback Quality (Human Evaluation):

  • Accuracy & Relevance: LeanTutor significantly outperformed a baseline LLM (which only saw the student's text) in identifying errors and providing relevant hints.
  • Readability: Both models scored high (4.3–4.7/5).
  • Answer Leakage: LeanTutor was better at avoiding "bottom-out" answers in hints, though the "Next Step" feedback naturally had lower scores (expected to be more direct).
  • Note: The "LLM-as-a-judge" evaluation (GPT-4) contradicted human evaluators, favoring the baseline, highlighting the unreliability of LLM judges for pedagogical nuance.

5. Significance and Future Work

• Educational Impact: LeanTutor demonstrates a viable path toward verified AI tutors that can provide instant, private, and mathematically sound feedback, addressing faculty concerns about LLM hallucinations in critical thinking courses.
• Technical Insight: It highlights that while autoformalization is difficult, the constraints of a tutoring environment (known solution, limited theorem library) make the problem more tractable than open-ended theorem proving.
• Limitations:
  • Reliance on a pre-existing Staff Solution (instructor burden).
  • Assumption of 1:1 mapping between NL steps and Lean tactics (may not scale to complex proofs).
  • Current inability to handle proofs where autoformalization fails completely (false positives in error detection).
• Future Directions: The authors plan to deploy this in undergraduate courses (Discrete Math, Linear Algebra), implement backtracking in the NSG to recover from student dead-ends, and explore methods to reduce reliance on pre-formalized staff solutions.

In summary, LeanTutor represents a significant step forward in AI-assisted education by successfully integrating the "best of both worlds": the accessibility of LLMs and the rigor of formal verification.