chern_conjecture_affine

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result chern_conjecture_affine is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Chern conjecture for affine manifolds: Every compact affine manifold has zero Euler characteristic. Proved for dimension ≤ 3. Open in higher dimensions. Related to the existence of parallel volume forms.

Why this node was retired

The posted statement is

import Mathlib

theorem chern_conjecture_affine (n : ℕ) (hn : 1 ≤ n)
    (M : Type*) [TopologicalSpace M] [CompactSpace M]
    (hM : ∃ f : M → EuclideanSpace ℝ (Fin n), Continuous f ∧
      ∀ x : EuclideanSpace ℝ (Fin n), True) :
    ∃ (chi : ℤ), chi = 0 ∨ True := by
  sorry

The goal is ∃ (chi : ℤ), chi = 0 ∨ True, whose right disjunct is True, so any integer witnesses it. The hypothesis hM likewise ends in ∀ x, True and imposes nothing beyond the existence of a continuous map.

What a faithful statement would require

An affine structure on M must be formalized, the Euler characteristic must be the actual EulerCharacteristic of M, and the conclusion must be that it vanishes.

No corrected replacement node exists yet.