Now

Last update: 2025-06-10

I have the privilege to lead the development of Lean’s standard library. This is a dream job: I get to play a key role in making Lean the best software verification tool there is, and I get to embark on this journey both as part of a great team at the Lean FRO as well as together with some amazing members of the Lean community.

I am convinced that a high-quality standard library will be an important piece of the puzzle making Lean the first truly economical formal methods tool. Therefore, I am thinking a lot both about real-world software verification in general and maintenance and QA for proof libraries in particular. I believe that achieving the highest quality standards is possible only with support from useful tools, and so I am building such a tool. Development is currently in an early stage. It is a very exciting time for me, because this is the first time I am building something this complex entirely from scratch.

Outside of work, I am a runner. Last autumn, I ran my first marathon in 3:05:46. In late September, I would like to break the three hour barrier. I ran a 15k in January that I was very happy with (56:54), but unfortunately I have had very long stretches of being sick since then, so I have not been able to do much training in the first half of 2025. I hope to get back into the full swing of training very soon.