This seminar will meet online, via Zoom, every Wednesday 14:00-15:30 (time may be changed later; first meeting is 17APR2024); 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 entry. 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.

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

Emilie Burgun wrote in Lean, during the semester, a formal proof of Rubin's reconstruction theorem.