Computer-Assisted Proofs

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 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:

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.