21-341: Linear Algebra
Grader
Instructor: Martin Rapaport
Fall 2026 · Carnegie Mellon University
Proof-based linear algebra. Graded homework and held weekly office hours.
Teaching Assistantship
Teaching is how I learn a subject twice. Here are the courses I've assisted with.
21-373 (A): Algebraic Structures
Grader
Instructor: Sharon Robins
Fall 2026 · Carnegie Mellon University
A first introduction to algebra. Graded homework and held weekly office hours.
Tutorials
Sessions I've run to get people started with the tools I work with, usually at a conference or while visiting another institution.
A practical introduction to theorem proving and formalisation in Lean
Workshop on AI for Mathematics · Tata Institute of Fundamental Research, Mumbai, India · 3–4 August 2026
Links to website and repository
A comprehensive, hands-on Lean tutorial spanning 8 hours over 4 sessions over 2 days. I briefly introduced important foundational properties that practically affect the way theorems and proofs are written in Lean; demonstrated various tactics; introduced different ways of writing definitions (such as structures and typeclasses); and explained important design choices and conventions (general and domain-specific) in Mathlib and downstream projects. I also talked a bit about how to get involved in open-source projects and shared some tips and pitfalls (with a brief demonstration) of using frontier LLMs for formalisation.
A brief introduction to Lean
Thematic Programme on AI for Mathematics · Korea Institute for Advanced Study, Seoul, South Korea · 16–17 July 2026
Link to website
A pop-up Lean tutorial offering a brief and practical introduction to Lean.