Here's the website where they kept track of the status of the Sphere Eversion Project: https://leanprover-community.github.io/sphere-eversion/

They have a dependency graph that shows the general structure of the argument: https://leanprover-community.github.io/sphere-eversion/bluep...