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-p

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/ https://leanprover-community.github.io/sphere-eversion/