LeanTutor: Towards a Verified AI Mathematical Proof Tutor

A mathematical proof tutor should be able to explain a mistake without inventing one. LeanTutor, presented in the AAAI proceedings' educational-AI track, explores a way to combine conversational language models with formal proof checking. The design is promising because it connects feedback to an external verifier. Its evaluation also shows why that connection does not automatically make the entire tutoring exchange correct.

Manooshree Patel and colleagues built three connected components. The first translates a natural-language proof into Lean, a language and system for checking mathematical reasoning. The second proposes a next proof step, and the third turns the resulting information into feedback that a learner can read. The intention is to let students work in ordinary mathematical language while the system uses formal structure behind the scenes.

The authors created PeanoBench, a dataset of 371 proofs based on elementary arithmetic tasks from the Natural Numbers Game. It includes correct proofs and deliberately altered proofs with missing steps. The natural-language versions were written by the paper's authors using different styles; they were not collected from a classroom of independent students. This makes the benchmark useful for controlled technical development while limiting how well it represents the variety of real learner explanations and errors.

A central evaluation question was whether the translated formal proof faithfully represented the submitted reasoning. A proof that successfully compiles is not enough: the model might have silently replaced a student's argument with a different valid solution. The researchers therefore compared individual tactics and resulting proof states with reference translations. They found that providing a formal staff solution helped, but also that the model relied heavily on that reference. Alternative reasoning paths remained difficult to translate reliably.

The end-to-end feedback evaluation was deliberately narrow. From incorrect proofs that had been successfully translated, the researchers selected twenty-one for evaluation. Two external graduate evaluators with mathematics-teaching experience rated feedback without knowing its model source; each proof was rated by one evaluator. LeanTutor's hints and suggested next steps received higher average accuracy and relevance scores than the language-model baseline. Readability was broadly comparable, and explicit next-step responses predictably revealed more of the answer. These are descriptive feedback ratings on a selected subset, not estimates of student learning gains.

The selection boundary is particularly important. The feedback assessment excluded proofs whose translation failed. In practice, a Lean error could arise from a student's mathematical mistake or from the system's own mistranslation. Confusing those cases could produce incorrect corrective feedback. The prototype also assumes a close correspondence between ordinary-language proof steps and formal tactics, and it relies on an already formalized staff solution. Those assumptions become harder to sustain as proofs grow more complex.

For mathematics educators and developers, LeanTutor identifies a useful direction: combine fluent explanations with tools that can check parts of the reasoning, and evaluate the connections between them. The next evidence needed is broader testing on authentic student work, transparent handling of uncertain translations, and classroom studies of independent proof construction. The paper offers an architectural and benchmark contribution, with a carefully bounded demonstration. It does not establish that the tutor is universally correct, improves retained understanding, or is ready to replace human feedback.