← All papers
Teaching Mathematics Using Lean and Controlled Natural Language
cs.LO
Sep 2, 2024 · v1
TL;DR
Presents Verbose Lean, a Lean 4 library for teaching proof-writing via controlled natural language.
Abstract
This paper presents Verbose Lean, a library leveraging Lean 4's flexibility to teach undergraduate mathematics students to read and write traditional paper proofs. Students write proofs that resemble natural language and are easy to transfer to paper. Teachers can customize the experience, and Lean 4's metaprogramming features allow creative pedagogical uses of a proof assistant.
Problem
Undergraduate mathematics students need to learn to read and write traditional paper proofs, but existing proof assistants produce proofs in formal syntax far removed from natural mathematical language.
Approach
Verbose Lean is a Lean 4 library that lets students write proofs resembling natural language, structured to transfer directly to paper. It leverages Lean 4's metaprogramming flexibility to allow teachers to customize the experience and create pedagogical exercises around proof-writing.
Results
Students produce proofs that are both machine-verified and readable as conventional mathematical prose. Teachers can adjust the level of formality and available tactics to match curricular goals.