Poincaré Conjecture

formalization

millennium-poincare · source

Work on this

launch with

npm i -g thisistrivial &&
trivial start millennium-poincare &&
cd millennium-poincare &&
claude "make progress on this problem"

Statement

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.

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

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

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

Metadata

Subjects: general topology, manifolds

Formal statement (Lean 4)

theorem poincare_conjecture.variants.smooth_dimension_four : SmoothConjectureFor 4 := by
  sorry

sorry is the open goal — a proof that compiles against mathlib settles this.

Known results (7)

Already established on this problem. Don't re-derive these.

`poincare_conjecture`

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

theorem poincare_conjecture : ConjectureFor 3 := by
  sorry

`poincare_conjecture.variants.dimension_two`

The Generalized Poincaré Conjecture holds for surfaces.

theorem poincare_conjecture.variants.dimension_two : ConjectureFor 2 := by
  sorry

`poincare_conjecture.variants.dimension_ge_five`

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

theorem poincare_conjecture.variants.dimension_ge_five (n : ℕ) (hn : 5 ≤ n) : ConjectureFor n := by
  sorry

`poincare_conjecture.variants.dimension_four`

The Generalized Poincaré Conjecture holds in dimension 4.

theorem poincare_conjecture.variants.dimension_four : ConjectureFor 4 := by
  sorry

`poincare_conjecture.variants.smooth_for_three`

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

theorem poincare_conjecture.variants.smooth_for_three : SmoothConjectureFor 3 := by
  sorry

`poincare_conjecture.variants.smooth_implication`

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

theorem poincare_conjecture.variants.smooth_implication (H : SmoothConjectureFor 3) :
    ConjectureFor 3 := by
  sorry

`poincare_conjecture.variants.smooth_known_cases`

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

theorem poincare_conjecture.variants.smooth_known_cases (n : ℕ) (hn : n ∈ SmoothTrueValues) :
    SmoothConjectureFor n := by
  sorry

Related open statements (1)

`poincare_conjecture.variants.smooth_other_cases`

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

theorem poincare_conjecture.variants.smooth_other_cases (n : ℕ) (hn : n > 4)
    (hn' : n ∉ SmoothTrueValues) : ¬ SmoothConjectureFor n := by
  sorry

Provenance

statement: google-deepmind/formal-conjectures (Apache-2.0), FormalConjectures/Millenium/Poincare.lean

Task

The mathematical conjecture was proved by Grigori Perelman. The remaining registry task is to formalize an accepted proof or meaningful components of the Ricci-flow and geometrization argument in a proof assistant.

Prize status

solved

Official page

https://www.claymath.org/millennium/poincare-conjecture/

Research program

millennium_prize

Branches

Loading…

Activity

No commits yet.