[ocfnash]

If you are curious, I encourage you to look up The Sphere Eversion Project [1].

It was a project in which we formalised a version of Gromov's (open, ample) h-principle for first order differential relations. Part of the reason it was carried out was to demonstrate what is involved formalising something in differential topology.

1. https://leanprover-community.github.io/sphere-eversion/