Bonn Lean seminar, summer semester 2026

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

Current schedule

Some details are subject to change.

• April 14. equality, transparency and all that (Fridolin)
• April 21. unification (Max)
• April 28. typeclass inference, part 1 (Abel)
• May 5. typeclass inference, part 2 (Alex)
• May 12. no seminar
• May 19. no seminar
• May 26. no seminar (holiday)
• June 2. integrals within integrals and the Sobolev inequality (Felix)
• June 6. the order of the talks is to be determined
  • Arend about qq, metaprogramming and ring
  • Evgenia about semantic engines and how they work
  • Johannes on verbose lean (and perhaps waterproof)
  • Pablo about the flypitch project and model theory
  • Pan on the positivity tactic
  • Vivek on simp, simp sets and simp normal forms
  • Yannik on the aesop tactic
• June 9. the mathlib contribution process (Ruth)
• June 16. the gcongr tactic (Pascal)
• June 23. no seminar
• June 30. no seminar
• July 7. to be determined
• July 9: the grind tactic (Hannah) room 0.007, joint with the formalised mathematics group seminar
• July 14. Doob's martingale convergence theorem (Shuhan)
• July 21. to be determined!