LeanTutor: Towards a Verified AI Mathematical Proof Tutor

TL;DR

LeanTutor is an AI-based proof tutor that combines large language models and theorem provers to provide a verified, natural language interface for learning formal mathematics, aiming to improve correctness and accessibility.

Contribution

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

Findings

Successful integration of LLMs and theorem provers in LeanTutor

PeanoBench enables systematic evaluation of proof tutoring systems

LeanTutor demonstrates potential for verified, natural language mathematical education

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.