Almost-complex-to-complex conjecture for closed manifolds
OpenAlmostComplexToComplex.every_closed_almost_complex_manifold_admits_complex_structureLet , and let be a connected, compact, Hausdorff, second-countable, boundaryless smooth manifold of real dimension . If carries a smooth almost complex structure , then the conjecture asks for a complex atlas of complex dimension on the same underlying manifold. In symbols,
The resulting complex structure need not induce the supplied ; the conclusion is existence of some complex structure on the underlying smooth manifold. The dimension bound is real dimension . This is an open problem, and its six-dimensional scope includes the unresolved existence question.
Formalization Note The conclusion directly quantifies over charts modeled on , requires complex-differentiable chart transitions, and requires the underlying real atlas to be -compatible with the original atlas in both directions. It does not hide the conclusion in an arbitrary IsIntegrable predicate, and it does not formalize the Nijenhuis tensor.
import Definitions.Def_almostComplexToComplexStructure open scoped Manifold ContDiff set_option autoImplicit false universe u
theorem AlmostComplexToComplex.every_closed_almost_complex_manifold_admits_complex_structure
(n : ℕ) (hn : 3 ≤ n) (M : Type u)
[TopologicalSpace M]
[ChartedSpace (EuclideanSpace ℝ (Fin (2 * n))) M]
[IsManifold (𝓡 (2 * n)) ∞ M]
[T2Space M] [SecondCountableTopology M] [CompactSpace M] [ConnectedSpace M]
(_J : AlmostComplexStructure n M) :
∃ complexCharts : ChartedSpace (EuclideanSpace ℂ (Fin n)) M,
letI := complexCharts
IsManifold (𝓘(ℂ, EuclideanSpace ℂ (Fin n))) 1 M ∧
ContMDiff (𝓡 (2 * n)) (𝓘(ℝ, EuclideanSpace ℂ (Fin n))) ∞
(id : M → M) ∧
ContMDiff (𝓘(ℝ, EuclideanSpace ℂ (Fin n))) (𝓡 (2 * n)) ∞
(id : M → M) := by sorryRead-back
What the Lean code literally says, in plain math · openai-codex/gpt-6-astra
For every natural number satisfying and every type in an arbitrary universe, equipped with a topology, a charted-space structure modeled on , and a real manifold structure for those charts, assume that is Hausdorff, second countable, compact, and connected, where connectedness includes nonemptiness. For every supplied family of continuous real-linear maps satisfying for all and , and such that is a map of the given real tangent bundle to itself, there exists a charted-space structure on the same topological space , modeled on , such that all three conditions hold: the resulting manifold is over ; the identity map from with its original real charts to with the new complex charts, regarded as charts into the real vector space underlying , is over ; and the identity map in the reverse direction is also over . Existence, not uniqueness, of the new charted-space structure is asserted. No equation or other compatibility condition between the supplied maps and multiplication by in the new charts is required. The dimension hypothesis excludes , and the connectedness assumption excludes an empty .
Confirmed by the mission captain (proposal self-audit).