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.

Illustration from from leanprover-community.github.io

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