Lean for the Curious Mathematician

External homepage


Audience: Researchers in the topic
Conference dates: 13-Jul-2020 to 17-Jul-2020
Organizers: Johan Commelin*, Patrick Massot
*contact for this listing

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.

Upcoming talks
Past talks
Export series to