This is your work, valued
math2001. Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
351Simons2025. Lecture notes and exercises for the 2025 Simons Foundation workshop "Lean for Mathematicians"
11metaprogramming. Tutorials for metaprogramming in Lean
10computations_in_lean. A tutorial on doing proofs with a computational flavour in the Lean proof assistant, and particularly on using the tactic polyrith
6symplectic. Group project at 2025 ICERM workshop "Autoformalization for the Working Mathematician"
3