Lean for the Curious Mathematician 2023

gm.general-mathematics
Start Date
2023-09-04
End Date
2023-09-07
Institution
Heinrich Heine University Düsseldorf
City
Düsseldorf
Country
Germany
Meeting Type
tutorial
Homepage
https://lftcm2023.github.io/tutorial/
Contact Name
Alexander Bentkamp, Jon Eugster, Immi Halupczok, Marcus Zibrowius
Created
Modified

Description

Are you curious what the excitement around the proof assistant Lean is all about? Are you intrigued by recent successes in the formalization of deep mathematical theorems, and would like to understand more concretely what this formalization entails? Do you find yourself wondering how far your favorite area of mathematics is still away from being formalized, and what lies ahead?

Then Lean for the Curious Mathematician is for you! The 2023 edition will comprise two consecutive but independent events: an intensive four-day tutorial (listed here), followed by a shorter colloquium for the impatient (listed separatedly).

Problems?

If you notice a problem with this entry, please contact the curators by email.