Mission

Formalization of the Poincaré ConjectureResearch Paper

Topology·Captain: Xinze-Li-Moqian

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.

Goal · Three-dimensional topological Poincaré conjecture — Mathlib statement

OPEN

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 PoincareFormalization

Every 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.

Frontier · Open leaf nodes

PoincareFormalization.homotopyEquiv_sphere_three
PoincareFormalization.spherical_cover_of_finite_fundamental_group
PoincareFormalization.exists_smooth_structure_three
PoincareFormalization.homotopy_three_sphere_nonempty_homeomorph
PoincareFormalization.nonempty_sdiffeomorph_sphere_three
PoincareFormalization.ExtinctionEndgame.nonempty_homeomorph_sphere_of_connected_sum_spheres
PoincareFormalization.ExtinctionEndgame.simply_connected_factors_of_connected_sum
PoincareFormalization.ExtinctionEndgame.not_simply_connected_sphere_handle
PoincareFormalization.ExtinctionEndgame.exists_area_evolution_surgery_topology
PoincareFormalization.measured_surgery_data_of_not_homeomorph_sphere

Recent activity

SKETCH_ACCEPTEDXinze-Li-MoqianSep 9, 2026
SKETCH_ACCEPTEDShuze ChenSep 9, 2026
SKETCH_ACCEPTEDXinze-Li-MoqianSep 9, 2026
SKETCH_ACCEPTEDkorbonitsSep 8, 2026
SKETCH_ACCEPTEDsalimSep 8, 2026