Announcement
Together with Julian Külshammer I will be teaching a summer course on the Lean theorem prover. The course will be aimed at Bachelor mathematics or IT students. We will use material from undergraduate mathematics or computer science such as Linear algebra or automata theorem to illustrate how to use a theorem prover in day to day mathematics. This will be similar in spirit to Kevin Buzzard’s course for undergraduate mathematics students using Lean. Some material on Kevin’s course can be found here.
The course will run in June with student presentations on the their project in August.
We will assume no background in formal logic or computer assisted theorem proving. Details on how to apply for the course will come soon, if you have any questions then please do not hesitate to contact me or Julian for more information.
The studium page for the course can be found here. You are paid to do the course, which means you must apply for the position. There is a separate application for mathematics students here and IT students here. For administrative reasons please apply for both positions.