This seminar will meet online, via Zoom, every Friday 14:00-15:30; the link is https://cs-uni-saarland-de.zoom.us/j/87336599438 and the password is the zipcode of the UdS campus. See also its LSF entries as proseminar and seminar. 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.
• A Mathematics in Lean, a course by Massot and Avigdad.
• A tutorials page by Patrick Massot.
• The seach entry point to mathlib.
• A Lean4 cheat sheet.
• A formal proof of Rubin's reconstruction theorem, written by Emilie Burgun during the WS 2023.

Tasks for next Friday (Nov 1, 2024):

• Play the natural number game, or any other game from the Lean game site (I think they're all good)
• Install Lean and mathlib on your computer, following these instructions; and then clone the "mathematics in Lean" book following these instructions.