My main areas of expertise revolve around the formalization of mathematics or the use of type theory to express ideas from mathematics or programming synthetically (via domain specific languages).
I often use Agda or Lean for formalization, or just work with pen-and-paper.
Here's a list of ideas that we can take as starting points, but please feel free to suggest other topics:
- Formalize topics from elementary group theory, combinatorics, or geometry in univalent foundations, in the style of the Symmetry book
- Formalize classical mathematical theorems for Lean's mathlib (preferably something you already understand)
- Formalize topics from category theory in univalent foundations (maybe for the 1lab)
- Explore topics within synthetic differential geometry (SDG) in type theory
- Explore topics within synthetic algebraic geometry in type theory à la Blechschmidt and the Synthetic Geometry project
- Explore topics within synthetic higher category theory in type theory à la Riehl–Shulman
- Explore aspects of distributed, probabilistic, or quantum computation by working in an appropriate internal language/type theory
Work
by