Formalisation of Mathematics

The masterclass will present recent advances in the formalisation of mathematics using the programming language Lean.

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 (https://github.com/leanprover-community/lean-liquid), which was recently completed, is one such project within the area of Condensed Mathematics. The goal of the masterclass is to present the results of the Liquid Tensor Experiment and teach participants the skills necessary to participate in such projects.

Speakers: 

  • Kevin Buzzard, Professor at Imperial College London.
  • Adam Topaz, Assistant Professor at the University of Alberta

Information on registration will follow in the Spring of 2023.
Contact: Dagur Tomas AsgeirssonBoris Bolvig Kjær

Illustration from from leanprover-community.github.io

Click the image for original graphics at leanprover-community.github.io