Masterclass: Formalisation of Mathematics
In recent years there has been a strong push towards formalising mathematics using proof assistants, allowing computers to formally verify the correctness of mathematical results. Proof assistants enable research collaborations on a whole new scale resembling the ways of modern software development. The Liquid Tensor Experiment (LTE), which was recently completed, is one such project within the area of Condensed Mathematics.
The goal of the masterclass is to build on the success of LTE and mark the beginning of condensed mathematics in Lean 4. The speakers will present aspects of LTE and provide opportunities for participants to contribute to new projects on a similar scale.
Click the image for original graphics at leanprover-community.github.io
- Kevin Buzzard, Professor at Imperial College London.
- Adam Topaz, Assistant Professor at the University of Alberta
PROGRAMME
| MO 26/6 | TU 27/6 | WE 28/6 | TH 29/6 | FR 30/6 | |
| 08:30-09:00 | Registration | ||||
| 9:00-10:00 | KB lecture 1 | KB lecture 2 | KB lecture 3 | KB lecture 4 | KB lecture 5 |
| 10:00-10:30 | Coffee/tea | Coffee/tea | Coffee/tea | Coffee/tea | Coffee/tea |
| 10:30-11:30 | AT lecture 1 | AT lecture 2 | AT lecture 3 | AT lecture 4 | AT lecture 5 |
| 11:30-13:00 |
Lunch |
Lunch |
Lunch |
Lunch |
Lunch |
| 13:00-14:00 |
Exercises and project work |
||||
| 14.00 | Coffee/tea | Coffee/tea | Coffee/tea | Coffee/tea | Coffee/tea |
| 15:00-16:00 |
Exercises and project work |
||||
| 18.00 | Reception Faculty Lounge 4th floor building 4, HCØ Room 04-4-19 |
Dinner: Food Club Vesterbro Vesterbrogade 6E, stuen 1620 København V |
|
||
Kevin Buzzard (KB), Adam Topaz. (AT)
All lectures are taking place in Aud. 10.
Participants are expected to be familiar with condensed mathematics (at least the first two Lectures in Scholze’s lecture notes: https://www.math.uni-bonn.de/people/scholze/Condensed.pdf), have some experience with formalisation of mathematics (not necessarily in Lean 4), and bring a computer with Lean 4 installed (https://leanprover.github.io/lean4/doc/quickstart.html).
The conference/masterclass will take place at the Department of Mathematical Sciences, University of Copenhagen. See detailed instructions on how to reach Copenhagen and the conference venue.
Tickets and passes for public transportation can be bought at the Copenhagen Airport and every train or metro station. You can find the DSB ticket office on your right-hand side as soon as you come out of the arrival area of the airport. DSB has an agreement with 7-Eleven, so many of their shops double as selling points for public transportation.
A journey planner in English is available.
More information on the "find us" webpage.
We kindly ask the participants to arrange their own accommodation.
We recommend Hotel 9 Små Hjem, which is pleasant and inexpensive and offers rooms with a kitchen. Other inexpensive alternatives are CabInn, which has several locations in Copenhagen: the Hotel City (close to Tivoli), Hotel Scandivania (Frederiksberg, close to the lakes), and Hotel Express (Frederiksberg) are the most convenient locations; the latter two are 2.5-3 km from the math department. Somewhat more expensive – and still recommended – options are Hotel Nora and Ibsen's Hotel.
An additional option is to combine a stay at the CabInn Metro Hotel with a pass for Copenhagen public transportation (efficient and reliable). See information about tickets & prices.
The deadline for funding applications is May 1 2023.
Registration for other participants end by June 11 2023
REGISTRATION HAS ENDED
Contact: Dagur Tomas Asgeirsson, Boris Bolvig Kjær
Admin: Jan Tapdrup jt@math.ku.dk
