London, UK

Heather Macbeth

Expert
@hrmacbeth
www.ma.imperial.ac.uk/~hmacbeth/

math2001. Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

351

Simons2025. Lecture notes and exercises for the 2025 Simons Foundation workshop "Lean for Mathematicians"

11

metaprogramming. Tutorials for metaprogramming in Lean

10

computations_in_lean. A tutorial on doing proofs with a computational flavour in the Lean proof assistant, and particularly on using the tactic polyrith

6

symplectic. Group project at 2025 ICERM workshop "Autoformalization for the Working Mathematician"

3
5
Apply