Using the proof assistant Lean in undergraduate mathematics classrooms

Gila Hanna, Brendan Larvor, Xiaoheng Yan

Research output: Contribution to journalArticlepeer-review


In this paper we develop a case for introducing a new teaching tool to undergraduate mathematics. Lean is an interactive theorem prover that instantly checks the correctness of every step and provides immediate feedback. Teaching with Lean might present a challenge, in that students must write their proofs in a formal way using a specific syntax. Accordingly, this paper addresses the issue of formalism from both a theoretical and a practical point of view. First, we examine the nature of proof, referring to historical and contemporary debates on formalization, and then show that in mathematical practice there is a growing rapprochement between strictly formal proof and proofs-in-practice. Next, we look at selections from the mathematics education literature that discuss how and when students advance through higher levels of mathematical maturity to reach a point at which they can cope with the demands of rigorous formalism. To probe the integration of Lean into teaching from an empirical point of view, we conducted an exploratory study that investigated how three undergraduate students approached the proof of double negation with Lean. The findings suggest that the rigorous nature of Lean is not an obstacle for students and does not stifle students’ creativity in writing proofs. On the contrary, proving with Lean offers a great deal of flexibility, allowing students to follow different paths to creating a valid proof.
Original languageEnglish
JournalZDM – Mathematics Education
Early online date22 Apr 2024
Publication statusE-pub ahead of print - 22 Apr 2024


  • Formalization of mathematics
  • Proof assistant, Lean prover
  • Proof construction
  • Rigorous and formal proofs
  • Undergraduate mathematics


Dive into the research topics of 'Using the proof assistant Lean in undergraduate mathematics classrooms'. Together they form a unique fingerprint.

Cite this