Conclusions
- A way to start formalizing with Lean:
- "Natural Number Game"
- helpful to master the thinking on the low
level
- "Mathematics in Lean"
- working through at least the first three
chapters and exercises
- → enough proficiency to cope with examples 1
and 2
-
"Formalising Mathematics"
- online course with a strong focus on
Mathlib
- explains the most important tactics and how to
apply them
- comes with a useful list of Lean tips
- skimming through the Mathlib files on matrices and
linear algebra
- asking concrete questions on the Lean Zulip chat
server
- Practicable for teaching?
- teaching to formalize proofs
- learning effort too high for first-year
students
- presenting formalized proofs
- could be helpful to understand structure and
logic of a proof
- example 1: how to find subgoals or organize
steps in a calculation
- example 2: how to cope with quantifiers in a
proof
- example 3: too difficult
- highly abstract formulation of Mathlib
- basic material from linear algebra still
missing
- What to do:
- learn it yourself - it's fun (for a
mathematician)
- use it to present clearer, better structured
proofs
- maybe present a few formalized proofs in the
lecture
- keep an open eye on the rapid development
