Using the Lean interactive theorem prover in undergraduate mathematics

• Xiaoheng Yan ^[1] ; Gila Hanna ^[1]
  1. [1] University of Toronto

     University of Toronto

     Canadá

     
• Localización: International journal of mathematical education in science and technology, ISSN 0020-739X, Vol. 56, Nº. 2, 2025, págs. 318-331
• Idioma: inglés
• DOI: 10.1080/0020739X.2023.2227191
• Enlaces
  • Texto completo
• Resumen

  • As new technological developments continue to change the educational landscape, it is not an exception in the area of proof and proving. This classroom note introduces the use of one of the trending proofs assistants – the Lean theorem prover. We first provide a technical account of Lean, then exemplify Lean proofs in propositional logic, number theory and real analysis to demonstrate its use and capacities for teaching and learning mathematics