This is the course webpage for Formalising Mathematics in Lean, an introductory course on the Lean programming language, a functional programming language that can be used as a proof verification system. The course is running in Spring 2024 under the auspices of the Glasgow-Maxwell School (GlaMS). The course team are Adrián Doña Mateo, Monica Abu Omar, Patrick Kinnear and Simone Castellan.

• When:

  Tuesdays, 10:00 to 11:30, starting on the 30th of January, 2024.

• Where:
  • Edinburgh: JCMB 5323
  • Glasgow: Room 309, Maths & Stats building

• Chat:

  Discord¹

• SSFM (Sporadic Seminars in Formalising Mathematics):

  To encourage one another to formalise, we will be holding sporadic seminars called Sporadic Seminars in Formalising Mathematics (SSFM). This can be online or in-person before/after each session.
  See more on the Discord server under (#ssfm) and the SSFM page here.

• Credit:

  For PhD students taking this course for credit², you will need to complete a (group) project. See the project page here for more information.
  But please speak to us before beginning your project, to discuss feasibility and credit-worthiness.