In 2021, I started contributing to Lean’s official mathematics library as a hobby. After completing my PhD in 2025, I am now again a regular contributor.
