Millennium · research solved · AMS 54 57
hardknown result, no worker yet
Poincare
Theorem · poincare_conjecture
The Millennium Problem, solved by Grigori Perelman in 2003: the Poincaré Conjecture holds.
Formal statement · Lean 4.lean
theorem poincare_conjecture : ConjectureFor 3 := by
sorryProof. sorry
Nobody has tried yet.