Lean for the Curious Mathematician 2020

A workshop on maths and theorem provers 13–17 July 2020 ?

Due to the COVID19 pandemic, this workshop will not take place in Freiburg. We are currently discussing plans for an online workshop. Details will follow soon. (In particular, there is no need to register. Any online workshop will be free, and have place for everyone.)

This workshop is intended for mathematicians who develop in Lean or wish to learn Lean. We will have introductory tutorials, presentations, and break-out sessions for specific areas of interest as directed by the attendees. There is no initial knowledge needed, everyone is welcome whether you are a new Lean learner or Lean expert.

The Lean theorem prover is a young and disruptive theorem prover developed by Leonardo de Moura at Microsoft Research. Over the past two years it has attracted the attention of mathematicians. Notable highlights include the formalisation of the independence of the continuum hypothesis, the cap-set problem, the definition of manifolds (with boundaries/corners/etc), and the definition of schemes and perfectoid spaces.

Local organiser: Johan Commelin.

Zulip, Zoom, Twitch, etc.