This is the repository for the advanced Lean seminar at university Bonn.
Prerequisites. Lean knowledge at the level of e.g. the lecture "Topics in Computer-assisted Mathematics" in WiSe25/26 (course page). The lecture will be offered again next winter; if you have not used Lean before, I recommend you take it first. If you have used Lean, but are unsure about your knowledge, feel free to write me an email (rothgang at math.uni-bonn.de).
Initial meeting. Thursday, February 12 at 10.15 (room 0.011).
Regular seminar time and place: Tuesdays, 14.15 to 15.45 (room N.008 --- in the Neubau building behind the main mathematics building). There will be a one-day block seminar on June 6, place to be announced.
Course page: ecampus; enrollment key leanonme
Outline and topics: see here
- April 14. Fridolin about equality, transparency and all that (slides, written documentation)
- April 21. Max about unification (handout, slides)
- April 28. Abel about typeclass inference, part 1(slides, written documentation)
- May 5. Alex about typeclass inference, part 2 (slides)
- May 12. no seminar
- May 19. no seminar
- May 26. no seminar (holiday)
- June 2. Felix about integrals within integrals and the Sobolev inequality (write-up)
- June 6. room N0.007; we meet from 10.15 until 13.30 at most
- June 9. Ruth about the mathlib contribution process (slides, handout)
- June 16. Pascal about the
gcongrtactic (slides, flow-chart of tactic logic, Lean example file, write-up focusing on the metaprogramming) - June 18. Pan about the
positivitytactic room 0.007, joint with the formalised mathematics group seminar (slides) - June 23. no seminar
- June 30. no seminar
- July 7. Pablo about the flypitch project and model theory (slides)
- July 9: Hannah about the
grindtactic room 0.007, joint with the formalised mathematics group seminar (slides, written documentation) - July 14. Shuhan on Doob's martingale convergence theorem (slides)
- July 21. Johannes on simp, simp sets and simp normal forms (write-up)
