1. FormalConjectures
  2. Millenium
  3. Poincare
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

The Poincaré Conjecture

References:

The formalisations in this file are based on the ones written by Junyan Xu in Mathlib4.

namespace PoincareConjecture open scoped Manifold ContDiff EuclideanGeometry ContinuousMap local macro:max "𝕊" noWs n:superscript(term) : term => `(Metric.sphere (0 : EuclideanSpace ℝ (Fin ($(⟨n.raw[0]⟩) + 1))) 1)

The predicate that the generalized Poincaré conjecture holds in dimension $n$, i.e. that any $n$-dimensional manifold that is homotopy equivalent to the sphere is in fact homeomorphic to the sphere.

def ConjectureFor (n : ℕ) : Prop := ∀ (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (ℝ^n) M], M ≃ₕ 𝕊n → Nonempty (M ≃ₜ 𝕊n)

The Millenium Problem, solved by Grigori Perelman in 2003: the Poincaré Conjecture holds.

@[category research solved, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture : ConjectureFor 3 := ⊢ ConjectureFor 3 All goals completed! 🐙

The Generalized Poincaré Conjecture holds for surfaces.

@[category textbook, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture.variants.dimension_two : ConjectureFor 2 := ⊢ ConjectureFor 2 All goals completed! 🐙

The Generalized Poincaré Conjecture holds for dimensions at least 5.

@[category textbook, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture.variants.dimension_ge_five (n : ℕ) (hn : 5 ≤ n) : ConjectureFor n := n:ℕhn:5 ≤ n⊢ ConjectureFor n All goals completed! 🐙

The Generalized Poincaré Conjecture holds in dimension 4.

@[category textbook, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture.variants.dimension_four : ConjectureFor 4 := ⊢ ConjectureFor 4 All goals completed! 🐙

The predicate that the smooth Poincaré conjecture holds in dimension $n$.

def SmoothConjectureFor (n : ℕ) : Prop := ∀ (M : Type) [TopologicalSpace M] [ChartedSpace (ℝ^n) M] [IsManifold (𝓡 n) ∞ M], M ≃ₕ 𝕊n → Nonempty (M ≃ₘ⟮𝓡 n, 𝓡 n⟯ 𝕊n)

A reformulation of the Millenium Problem in terms of smooth 3-folds.

@[category textbook, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture.variants.smooth_for_three : SmoothConjectureFor 3 := ⊢ SmoothConjectureFor 3 All goals completed! 🐙

The smooth formulation of the Millenium Problem implies the general case. This follows from the fact that every topological 3-fold admits a smooth structure [mo296171].

@[category textbook, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture.variants.smooth_implication (H : SmoothConjectureFor 3) : ConjectureFor 3 := H:SmoothConjectureFor 3⊢ ConjectureFor 3 All goals completed! 🐙

The values at which the smooth version of the conjecture is known to hold.

def SmoothTrueValues : Set ℕ := {1, 2, 3, 5, 6, 12, 56, 61}

The smooth version of the Poincaré conjecture is known to hold in dimensions $1, 2, 3, 5, 6, 12, 56, 61$. See [Wang2017].

@[category research solved, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture.variants.smooth_known_cases (n : ℕ) (hn : n ∈ SmoothTrueValues) : SmoothConjectureFor n := n:ℕhn:n ∈ SmoothTrueValues⊢ SmoothConjectureFor n All goals completed! 🐙

The four dimensional case of the smooth version of the conjecture is still open. See [Wang2017].

@[category research open, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture.variants.smooth_dimension_four : SmoothConjectureFor 4 := ⊢ SmoothConjectureFor 4 All goals completed! 🐙

It is conjectured that the only values of $n > 4$ for which the smooth version of the conjecture holds are $n = 5, 6, 12, 56, 61$. See Conjecture 1.17 in [Wang2017].

@[category research open, AMS 54 57] theorem declaration uses 'sorry'poincare_conjecture.variants.smooth_other_cases (n : ℕ) (hn : n > 4) (hn' : n ∉ SmoothTrueValues) : ¬ SmoothConjectureFor n := n:ℕhn:n > 4hn':n ∉ SmoothTrueValues⊢ ¬SmoothConjectureFor n All goals completed! 🐙 end PoincareConjecture