Zulip Chat Archive

Stream: sphere eversion

Topic: Local theory

Patrick Massot (Apr 13 2022 at 17:43):

Big sphere eversion project update: Chapters 1 and 2 are now completely sorry-free! This means the local version of flexibility of open and ample differential relations is completely formalized. On paper the remaining step is: "this local statement obviously implies the global statement". I'm cheating slightly because the trick to get parameters for free is only stated globally in the blueprint, so technically we only proved the local statement without parameters. Anyway, the remaining work is 100% about proving the manifold library in mathlib is actually usable.

Johan Commelin (Apr 13 2022 at 18:12):

Fantastic news!

Kevin Buzzard (Apr 13 2022 at 18:50):

Congratulations! It will be great to have a serious consumer of the manifold library.

Last updated: Dec 20 2023 at 11:08 UTC