# Lean for the curious mathematician

A virtual workshop on computer-checked mathematics — [13–17 July 2020]

## Description

Lean is a proof assistant.
This means that you can use it to explain mathematics to a computer, and the
computer will check everything makes sense.
This workshop is intended for mathematicians who use 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.
Experienced users will be available to answer questions, supervise
exercises sessions, and participate in pair programming.

There is no initial knowledge needed; everyone is welcome.
Intermediate users will be able to start pair programming immediately
while beginners will first learn the basics, including installing the
software and its supporting tools.

## Why Lean?

The Lean theorem prover is a young theorem prover
developed mostly 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.

Beyond technical aspects, a large part of Lean’s appeal to
mathematicians comes from its very active and friendly
community of users which,
compared to other proof assistants, has a very strong focus on
mathematics instead of computer science and software engineering.

## Organisation

Although this event was originally intended to happen in Freiburg, the
Covid pandemic turned it into a *virtual* meeting.
See the participants and schedule
pages for details.

Main organisation by:
Johan Commelin and
Patrick Massot.

Feel free to contact us on
Zulip.