I’m a PhD student on the Vidi Grant Lean Forward under the supervision of Jasmin Blanchette. My research is about making dependently-typed proof assistants more user-friendly. In particular, I develop proof automation for the Lean theorem prover.