LeanTutor: Towards a Verified AI Mathematical Proof Tutor

TL;DR

LeanTutor is an AI-based mathematical proof tutor that combines large language models and theorem provers to provide verified, natural language feedback for learning formal proofs in Peano Arithmetic.

Contribution

The paper introduces LeanTutor, a novel system integrating LLMs and theorem provers for verified mathematical tutoring, along with a new dataset PeanoBench for evaluation.

Findings

LeanTutor can generate next proof steps with high accuracy.

The system provides natural language feedback aligned with formal proofs.

PeanoBench enables benchmarking of AI proof tutoring systems.

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.