ICTS:31592

Video URL

Lean for Teaching

Lean for Teaching

(2025). Lean for Teaching. SciVideos. https://youtu.be/ghOPE4Q8MxM

Lean for Teaching. SciVideos, Apr. 26, 2025, https://youtu.be/ghOPE4Q8MxM 

          @misc{ scivideos_ICTS:31592,
            doi = {},
            url = {https://youtu.be/ghOPE4Q8MxM},
            author = {},
            keywords = {},
            language = {en},
            title = {Lean for Teaching},
            publisher = {},
            year = {2025},
            month = {apr},
            note = {ICTS:31592 see, \url{https://scivideos.org/index.php/icts-tifr/31592}}
          }
Patrick Massot
Talk numberICTS:31592
Source RepositoryICTS-TIFR
Collection

Abstract

I will describe how the Lean proof assistant software can be used to teach mathematical reasoning to young students at university. This is different from teaching how to use Lean. Here Lean is only a tool, not the end goal.

I will explain what we can hope to teach using this tool, what are the available resources for teachers, and what choices should be made. I will then show my teaching library, Verbose Lean, which uses controlled natural language and customizable automation to optimize transfer of skills to paper proofs.