This seminar will meet online, via Zoom, every Wednesday 14:00-15:30. Please drop me an email (bartholdi@math.uni-sb.de) to obtain the link, or get it from lsf. It is offered to anyone interested, in particular maths and computer science students.

The goal of the seminar is to practice using the computer system Lean to write computer-assisted proofs in mathematics. Some useful links:

• The main Lean entry point.
• Zulipchat, the forum for all Lean/mathlib-related discussions.
• The natural number game, in LEAN4.
• Kevin Buzzard's natural number game, a good way to start learning Lean.
• A course at Imperial College on formalizing mathematics with Lean; with course notes.
• A tutorial by Patrick Massot
• The seach entry point to mathlib.

I will post further information on this site as the semester progresses.