Proof assistants are a way to use a computer to prove a theorem or formally verify a piece of code, instead of for numerical calculations or algebraic manipulations. They have a long history dating back to the 50s, but have recently gained a lot of tractions with Gonthier et. al.'s proofs of the four colour theorem in 2005 and the odd-order theorem in 2013, Hales’ formal proof of the Kepler conjecture in 2014, and verification of an essential part of Clausen–Scholze’s condensed mathematics by Johan Commelin et al. in 2021. The rising interest in interactive theorem proving in the mathematics community can also be seen from the invitation of Kevin Buzzard as plenary speaker of the ICM this year.

Among the most accessible proof assistants is the Lean theorem prover, developed by Leonardo de Moura at Microsoft Research. To get an impression of how it feels like to prove a theorem in a proof assistant, we recommend the applicants to try out some of the induction proofs in https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/.

The goal of the Summer Camp 2022, joint between maths and IT, will be (after some introductory lectures by Justin Pearson and Julian Külshammer) that the participants write a small project in Lean formally verifying a small piece of mathematics or computer science with the help of Lean. Topics will be decided jointly together with the participants and could for example be from automata theory, single variable calculus or elementary number theory. We will assume no background in formal logic or computer assisted theorem proving. 

The Summer Camp 2022 will run throughout June 2022, after the exams of the participants have ended. It will end with some oral presentations of the projects by the participants. The participants will be employed by the University on the level of research assistant. To apply please follow the following links to the application Varbi. For organisational reasons, we would like you to submit an application to both positions. 

https://uu.se/jobb/detaljsida/?positionId=496772

https://uu.se/jobb/detaljsida/?positionId=501831

Any inquiries then please contact  Justin Pearson or Julian Külshammer