I am a Research Software Engineer/Tech Lead at the Lean FRO and a mathlib maintainer.
- π Iβm currently working on the Lean programming language and theorem prover
- π± Iβm currently learning basic Isabelle/HOL and advanced category theory
- π― Iβm looking to collaborate on formalizing ind-objects in mathlib (send me a message on Zulip)
- π¬ Ask me about how to build software that actually works (I don't know, but I'd love to hear your thoughts)
- π« How to reach me: send me a message on Zulip
- π Pronouns: he/him