Friday, 25 April 2025
Mathlib is a vast and constantly growing library of formalized mathematics. As its size increases, it becomes increasingly easy to spend a significant amount of time formalizing a theorem, only to later discover that it was already present in the library. This can be both frustrating and discouraging. In this talk, we will introduce and demonstrate a variety of tools and techniques that can help users efficiently navigate Mathlib, search for existing results, and better understand the structure of the library.
Mathematicians have trained themselves to see objects from many points of view. When considering the real numbers, we can as easily see them as equivalence classes of Cauchy sequences, or Dedekind cuts, or the unique uniformly complete Archimedean field. The computer is not as forgiving and forces us to pick a particular definition that we must stick with. Using examples from the Lean mathematical library, Mathlib, I investigate why it is so important to choose the right definition when formalizing, what makes formal definitions look different from pen and paper definitions, and how we can design our definitions to make proofs flow smoothly.
Saturday, 26 April 2025
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.