Lean metaprogrammer at the Mathlib Initiative. Background in math & physics. Tree, cloud, and music appreciator. Has a passion for existing.