LIPIcs.ITP.2024.27.pdf
- Filesize: 0.65 MB
- 19 pages
Document
Teaching Mathematics Using Lean and Controlled Natural Language
Author
Patrick Massot 
-
Part of:
Volume:
15th International Conference on Interactive Theorem Proving (ITP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-02
File
Document Identifiers
Author Details
Acknowledgements
The library described here is the result of work spread over five years and benefited from many interactions. Marie-Anne Poursat made it possible by trusting me to teach using a proof assistant. Frédéric Bourgeois and Christine Paulin-Mohring later joined me in teaching this course and discussing how to make it more useful. Our students also participated with their patience, questions and enthusiasm. Very recently, Julien Narboux, Pierre Boutry and Evmorfia-Iro Bartzia started using this library with students and made valuable comments. Simon Hudon started my Lean meta-programming education. It was then continued by Mario Carneiro and Kyle Miller who both also directly contributed crucial code that I would have been incapable of writing. Wojciech Nawrocki helped me a lot with widgets, adding several features to his ProofWidgets library for the needs of this project. More generally many people from the Mathlib community contributed indirectly by formalizing basic mathematics and creating tactics that we built on. I also benefited from conversations about teaching using a proof assistant, particularly with Heather Macbeth, Jim Portegies and Jelle Wemmenhove. Most of the work on the Lean 4 version was made possible by Jeremy Avigad’s invitation to benefit from some of Charles Hoskinson’s generous donation to CMU. And of course none of this would exist without the amazing work of Leonardo de Moura and Sebastian Ullrich on Lean 4.
Cite AsGet BibTex
Patrick Massot. Teaching Mathematics Using Lean and Controlled Natural Language. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.27
https://doi.org/10.4230/LIPIcs.ITP.2024.27
Abstract
We present Verbose Lean, a library using the flexibility of the Lean programming language and proof assistant to teach undergrad mathematics students how to read and write traditional paper proofs. After explaining our main pedagogical goals, we explain how students use the library with varying levels of assistance to write proofs that are easy to transfer to paper because they look like natural language. We then describe how teachers can customize the student experience based on their specific pedagogical goals and constraints. Finally we describe some aspects of the implementation of the library, emphasizing how new aspects of the very recently released version 4 of Lean allow a lot of flexibility that could benefit many new creative uses of a proof assistant.
Subject Classification
ACM Subject Classification
- Human-centered computing → Natural language interfaces
- Applied computing → Interactive learning environments
- Theory of computation → Logic and verification
Keywords
- mathematics teaching
- proof assistant
- controlled natural language
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Jeremy Avigad. Learning Logic and Proof with an Interactive Theorem Prover, pages 277-290. Springer International Publishing, Cham, 2019. URL: https://doi.org/10.1007/978-3-030-28483-1_13.
- Evmorfia-Iro Bartzia, Emmanuel Beffara, Antoine Meyer, and Julien Narboux. Underlying theories of proof assistants and potential impact on the teaching and learning of proof. In 12th International Workshop on Theorem proving components for Educational software, Rome, Italy, July 2023. Julien Narboux and Walther Neuper and Pedro Quaresma. URL: https://hal.science/hal-04227823.
- Merlin Carl. Number theory and axiomatic geometry in the diproche system. In Pedro Quaresma, Walther Neuper, and João Marcos, editors, Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020, volume 328 of EPTCS, pages 56-78, 2020. URL: https://doi.org/10.4204/EPTCS.328.4.
- Merlin Carl, Hinrich Lorenzen, and Michael Schmitz. Natural language proof checking in introduction to proof classes - first experiences with diproche. In João Marcos, Walther Neuper, and Pedro Quaresma, editors, Proceedings 10th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2021, (Remote) Carnegie Mellon University, Pittsburgh, PA, United States, 11 July 2021, volume 354 of EPTCS, pages 59-70, 2021. URL: https://doi.org/10.4204/EPTCS.354.5.
- Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
- Pablo Donato, Pierre-Yves Strub, and Benjamin Werner. A drag-and-drop proof tactic. In Andrei Popescu and Steve Zdancewic, editors, CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 197-209. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503692.
-
Marie Kerjean, Frédéric Le Roux, Patrick Massot, Micaela Mayero, Zoé Mesnil, Simon Modeste, Julien Narboux, and Pierre Rousselin. Utilisation des assistants de preuves pour l'enseignement en L1. In Gazette de la SMF, volume 174, Octobre 2022.
- Heather Macbeth. The mechanics of proof. URL: https://hrmacbeth.github.io/math2001/.
- Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An extensible user interface for Lean 4. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 of LIPIcs, pages 24:1-24:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ITP.2023.24.
- Benoît Rognier. Edukera. URL: https://edukera.com/.
- Frédéric Le Roux. D∀∃duction. URL: https://perso.imj-prg.fr/frederic-leroux/d%E2%88%83%E2%88%80duction/.
- Athina Thoma and Paola Iannone. Learning about proof with the theorem prover Lean: the abundant numbers task. International Journal of Research in Undergraduate Mathematics Education, 8(1):64-93, April 2022. URL: https://doi.org/10.1007/s40753-021-00140-1.
- Sebastian Ullrich. An Extensible Theorem Proving Frontend. PhD thesis, Karlsruhe Institute of Technology, Germany, 2023. URL: https://nbn-resolving.org/urn:nbn:de:101:1-2023080204582480933072, URL: https://doi.org/10.5445/IR/1000161074.
- Sebastian Ullrich and Leonardo de Moura. Beyond notations: Hygienic macro expansion for theorem proving languages. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:1)2022.
- Sebastian Ullrich and Leonardo de Moura. 'do' unchained: embracing local imperativity in a purely functional language (functional pearl). Proc. ACM Program. Lang., 6(ICFP):512-539, 2022. URL: https://doi.org/10.1145/3547640.
- Jelle Wemmenhove, Thijs Beurskens, Sean McCarren, Jan Moraal, David Tuin, and Jim Portegies. Waterproof: educational software for learning how to write mathematical proofs, 2022. URL: https://arxiv.org/abs/arXiv:2211.13513.
- Xiaoheng Yan and Gila Hanna. Using the Lean interactive theorem prover in undergraduate mathematics. International Journal of Mathematical Education in Science and Technology, 0(0):1-15, 2023. URL: https://doi.org/10.1080/0020739X.2023.2227191.