Mission
Formalization of the Poincaré Conjecture
Log in to contributeGoal
Our goal
This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's Notes on Perelman's Papers.
Important references
Poincare-Conjecture and DifferentialGeometry are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.
OpenGA's role
OpenGA focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.
The PoincareConjecture directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.
We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.
namespace PoincareFormalization
theorem nonempty_homeomorph_sphere_three (M : Type*) [TopologicalSpace M]
[T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]
[SimplyConnectedSpace M] [CompactSpace M] :
Nonempty (M ≃ₜ ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (3 + 1))) 1)) := by
sorry
end PoincareFormalizationEvery compact simply connected Hausdorff topological 3-manifold without boundary is homeomorphic to the unit 3-sphere in Euclidean 4-space. This follows the exact hypotheses and conclusion of Mathlib’s proof_wanted SimplyConnectedSpace.nonempty_homeomorph_sphere_three; only the declaration namespace and local notation are adapted for this platform. No extra second-countability assumption is imposed.