I have some experience with formalising Mathematics in the Lean theorem prover. In particular, I have made pull requests to the mathematics library mathlib. In particular, I wrote a significant proportion of the library about the fundamental groupoid of a topological space.