Add the Hopf problem (complex structure on the 6-sphere)

[Deicyde]

Closes #5110.

Adds FormalConjectures/Paper/HopfProblem.lean: the Hopf problem (Hopf, 1948) — does the 6-sphere admit a complex structure? — stated as a research open question in the answer(sorry) ↔ form, since the problem is open in both directions:

@[category research open, AMS 32 53]
theorem hopf_problem :
    answer(sorry) ↔
      ∃ cs : ChartedSpace (EuclideanSpace ℂ (Fin 3))
        (Metric.sphere (0 : EuclideanSpace ℝ (Fin 7)) 1),
        letI := cs
        IsManifold 𝓘(ℂ, EuclideanSpace ℂ (Fin 3)) ω
          (Metric.sphere (0 : EuclideanSpace ℝ (Fin 7)) 1) := by
  sorry

Formalisation notes

• "Complex structure" = holomorphic atlas. The existential asks for a ChartedSpace structure modeled on ℂ³ making the sphere an analytic (ω) manifold over ℂ, Mathlib's rendering of "complex manifold" (cf. UpperHalfPlane's IsManifold 𝓘(ℂ) ω instance).
• Topological rather than smooth S⁶. No compatibility with the standard smooth atlas is demanded. This is equivalent to the classical statement (an integrable almost complex structure on the smooth S⁶): any complex manifold whose underlying space is S⁶ is a smooth homotopy 6-sphere, hence diffeomorphic to the standard S⁶ (Smale's h-cobordism theorem plus Θ₆ = 0, Kervaire–Milnor); conversely integrable almost complex structures yield holomorphic atlases by Newlander–Nirenberg. Avoiding the compatibility condition keeps the statement free of restriction-of-scalars bookkeeping between ℂ³- and ℝ⁶-modeled atlases.
• No degenerate witnesses. ChartedSpace charts are (open) partial homeomorphisms covering the nonempty sphere, so the existential cannot be satisfied vacuously; demanding ω rather than C¹ adds no strength over ℂ.

Verified with lake build FormalConjectures.Paper.HopfProblem (only the expected sorry).

Related work: deancureton/sphere-six-complex (Cureton & Lezeau, created 2026-08-23) is an active formalization of Alpöge's claimed construction, with its own challenge statement in the stronger smooth-compatible form (underlying real atlas diffeomorphic to the standard one); the statement in this PR is the minimal topological form, equivalent by Smale + Θ₆ = 0 as discussed above, and independent of any particular claimed resolution.

Disclosure: formalised with the assistance of Claude (Anthropic), at my request and reviewed by me.

🤖 Generated with Claude Code

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[Paul-Lez]

Sick, @deancureton and I are currently working on formalising the solution to this here: https://github.com/deancureton/sphere-six-complex