English
For a given natural number n, the smooth Poincaré conjecture asserts that if a smooth n-manifold M is diffeomorphic to the standard n-sphere S^n, then M is smoothly diffeomorphic to S^n. The conjecture is known to be true for n ∈ {1,2,3,5,6,12,56,61}, open for n=4, and (conjecturally) no other n>4 satisfy the property.
Русский
Для заданного числа n гладкая гипотеза Пуанкаре утверждает, что если гладкая n-мерная многообразие M гладово эквивалентно стандартной сфере S^n, то существует гладкая диффеоморфизм M ≅ S^n. Гипотеза доказана для n ∈ {1,2,3,5,6,12,56,61}, для n=4 открыта, и предполагается, что для других n>4 такого свойства нет.
LaTeX
$$$$\\text{Для каждого }n\\in\\mathbb{N}:\\; \\text{NonemptyDiffeomorphSphere}(n)\\ \\text{ означает, что каждый гладкий }n\\text{-манифолд, который гомеоморфен }S^n, \\text{ имеет гладкий диффеоморфизм }M\\cong S^n.$$ \n\\text{Истина для }n\\in\\{1,2,3,5,6,12,56,61\\},\\; \\text{открыто для }n=4,\\; \\text{нет оснований считать существование таких }n>4. $$$$
Lean4
/-- The smooth Poincaré conjecture; true for n = 1, 2, 3, 5, 6, 12, 56, and 61,
open for n = 4, and it is conjectured that there are no other n > 4 for which it is true
(Conjecture 1.17, https://annals.math.princeton.edu/2017/186-2/p03). -/
def NonemptyDiffeomorphSphere (n : ℕ) : Prop :=
∀ (_ : ChartedSpace (ℝ ⁿ) M) (_ : IsManifold (𝓡 n) ∞ M), (M ≃ₕ 𝕊 ⁿ) → Nonempty (M ≃ₘ⟮𝓡 n, 𝓡 n⟯ 𝕊 ⁿ)
