This workshop is aimed primarily at PhD students with an interest in formalising results from algebraic geomery using the Lean theorem prover. Participants will work in teams on formalisation projects designed by our guest speakers.
To apply for the workshop please send an email to
lean-workshop@mathi.uni-heidelberg.debefore October 10th (see Prerequisites for details).
Workshop Details
- Speakers / Project Leaders:
- Christian Merten (Utrecht University).
- Junyan Xu (Heidelberg University).
- Andrew Yang (Imperial College London).
- Dates: 19-21 November 2025.
- Location: Mathematikon, Heidelberg University.
Prerequisites
- Participants should have prior familiarity with algebraic geometry, at the level of a Master degree in the field.
- When it comes to prior Lean experience, we expect participants to have played the Natural Number Game and to have worked through the Chapters 2, 3, 4, 7 and 8 of the online textbook Mathematics in Lean.
- When applying for the workshop, please describe your background in algebraic geometry as well as your experience in Lean.