Import the Hopf problem formalization

LeanPool.lean

@@ -1926,6 +1926,153 @@ import LeanPool.HansonWright.Probability.Moments.Cumulant
 import LeanPool.HansonWright.Probability.Moments.Exponential
 import LeanPool.HansonWright.Probability.Process.FiniteMaximum
 import LeanPool.HansonWright.Probability.Process.SubGaussian
+import LeanPool.HopfProblem
+import LeanPool.HopfProblem.CuspFibre.CuspBoundaryTopVanishing
+import LeanPool.HopfProblem.CuspFibre.CuspCentralHomology1
+import LeanPool.HopfProblem.CuspFibre.CuspCentralHomology2
+import LeanPool.HopfProblem.CuspFibre.CuspCentralHomology3
+import LeanPool.HopfProblem.CuspFibre.CuspCentralHomology4
+import LeanPool.HopfProblem.CuspFibre.CuspNegation
+import LeanPool.HopfProblem.CuspFibre.CuspPositiveRetraction
+import LeanPool.HopfProblem.CuspFibre.CuspSpecialization
+import LeanPool.HopfProblem.Elliptic.Core1
+import LeanPool.HopfProblem.Elliptic.Core2
+import LeanPool.HopfProblem.Elliptic.Core3
+import LeanPool.HopfProblem.Elliptic.Core4
+import LeanPool.HopfProblem.Elliptic.Core5
+import LeanPool.HopfProblem.Elliptic.Core6
+import LeanPool.HopfProblem.Elliptic.Core7
+import LeanPool.HopfProblem.Elliptic.Core8
+import LeanPool.HopfProblem.Foundations.CanonicalProduct
+import LeanPool.HopfProblem.Foundations.Complex
+import LeanPool.HopfProblem.Foundations.Core1
+import LeanPool.HopfProblem.Foundations.Core2
+import LeanPool.HopfProblem.Foundations.Core3
+import LeanPool.HopfProblem.Foundations.Core4
+import LeanPool.HopfProblem.Foundations.Core5
+import LeanPool.HopfProblem.Foundations.EuclideanSphere
+import LeanPool.HopfProblem.Foundations.FibreTopology
+import LeanPool.HopfProblem.Foundations.InvariantSubsetQuotient
+import LeanPool.HopfProblem.Foundations.LineBundleTransport
+import LeanPool.HopfProblem.Foundations.LocalOrbitQuotient
+import LeanPool.HopfProblem.Foundations.PeriodTorusTypeOneOne
+import LeanPool.HopfProblem.Foundations.SplitGroupExtension
+import LeanPool.HopfProblem.Foundations.TrianglePeriodFamilyHomologySplitting
+import LeanPool.HopfProblem.Foundations.TriangleRegularBaseFundamentalGroup
+import LeanPool.HopfProblem.Foundations.TwoAffineCharts
+import LeanPool.HopfProblem.Foundations.TwoOpenTransition
+import LeanPool.HopfProblem.HomologyOfX.CuspCoinvariants
+import LeanPool.HopfProblem.HomologyOfX.SmallChainBiprod
+import LeanPool.HopfProblem.HomologyOfX.ThreefoldGluing1
+import LeanPool.HopfProblem.HomologyOfX.ThreefoldGluing2
+import LeanPool.HopfProblem.HomologyOfX.ThreefoldHomology1
+import LeanPool.HopfProblem.HomologyOfX.ThreefoldHomology2
+import LeanPool.HopfProblem.HomologyOfX.ThreefoldHomology3
+import LeanPool.HopfProblem.HomologyOfX.ThreefoldHomology4
+import LeanPool.HopfProblem.HomologyOfX.ThreefoldHomologyStarCoproduct
+import LeanPool.HopfProblem.HomologyOfX.TrianglePeriodFamilyHomologyAlgebra
+import LeanPool.HopfProblem.HomologyOfX.TrianglePeriodFamilyHomologyLattice
+import LeanPool.HopfProblem.HomologyTheory.FirstHurewicz1
+import LeanPool.HopfProblem.HomologyTheory.FirstHurewicz2
+import LeanPool.HopfProblem.HomologyTheory.FirstHurewicz3
+import LeanPool.HopfProblem.HomologyTheory.SingularMayerVietoris
+import LeanPool.HopfProblem.HomologyTheory.SphereHomology1
+import LeanPool.HopfProblem.HomologyTheory.SphereHomology2
+import LeanPool.HopfProblem.HomologyTheory.SphereHomology3
+import LeanPool.HopfProblem.Hurewicz.HigherHurewicz1
+import LeanPool.HopfProblem.Hurewicz.HigherHurewicz2
+import LeanPool.HopfProblem.Hurewicz.SecondHurewicz
+import LeanPool.HopfProblem.Hurewicz.SixthHurewicz
+import LeanPool.HopfProblem.Hurewicz.ThirdHurewicz
+import LeanPool.HopfProblem.Lattice.Core1
+import LeanPool.HopfProblem.Lattice.Core2
+import LeanPool.HopfProblem.MainTheorem.Core1
+import LeanPool.HopfProblem.MainTheorem.Core2
+import LeanPool.HopfProblem.MainTheorem.Core3
+import LeanPool.HopfProblem.MainTheorem.SixSphereCube1
+import LeanPool.HopfProblem.MainTheorem.SixSphereCube2
+import LeanPool.HopfProblem.MainTheorem.SixSphereCube3
+import LeanPool.HopfProblem.PeriodFamily.Core1
+import LeanPool.HopfProblem.PeriodFamily.Core2
+import LeanPool.HopfProblem.PeriodFamily.Core3
+import LeanPool.HopfProblem.PeriodFamily.Core4
+import LeanPool.HopfProblem.PeriodFamily.Core5
+import LeanPool.HopfProblem.PeriodFamily.Core6
+import LeanPool.HopfProblem.PeriodFamily.Core7
+import LeanPool.HopfProblem.PeriodFamily.Core8
+import LeanPool.HopfProblem.PeriodFamily.Core9
+import LeanPool.HopfProblem.PeriodFamily.HolomorphicPeriodMap1
+import LeanPool.HopfProblem.PeriodFamily.HolomorphicPeriodMap2
+import LeanPool.HopfProblem.PeriodFamily.PeriodDomain
+import LeanPool.HopfProblem.PeriodFamily.PeriodPoint
+import LeanPool.HopfProblem.Pi1.FundamentalGroupVanKampen1
+import LeanPool.HopfProblem.Pi1.FundamentalGroupVanKampen2
+import LeanPool.HopfProblem.Pi1.MappingTorus
+import LeanPool.HopfProblem.Pi1.MappingTorusHomology
+import LeanPool.HopfProblem.Pi1.ThreefoldOverlapMappingTorus1
+import LeanPool.HopfProblem.Pi1.ThreefoldOverlapMappingTorus2
+import LeanPool.HopfProblem.Pi1.TwistGroup
+import LeanPool.HopfProblem.Prelude
+import LeanPool.HopfProblem.Recognition.Degree1
+import LeanPool.HopfProblem.Recognition.Degree2
+import LeanPool.HopfProblem.Recognition.Degree3
+import LeanPool.HopfProblem.Recognition.Smale1
+import LeanPool.HopfProblem.Recognition.Smale10
+import LeanPool.HopfProblem.Recognition.Smale11
+import LeanPool.HopfProblem.Recognition.Smale12
+import LeanPool.HopfProblem.Recognition.Smale13
+import LeanPool.HopfProblem.Recognition.Smale2
+import LeanPool.HopfProblem.Recognition.Smale3
+import LeanPool.HopfProblem.Recognition.Smale4
+import LeanPool.HopfProblem.Recognition.Smale5
+import LeanPool.HopfProblem.Recognition.Smale6
+import LeanPool.HopfProblem.Recognition.Smale7
+import LeanPool.HopfProblem.Recognition.Smale8
+import LeanPool.HopfProblem.Recognition.Smale9
+import LeanPool.HopfProblem.Threefold.SixSphereComplexAtlas
+import LeanPool.HopfProblem.Threefold.SpecialPeriods1
+import LeanPool.HopfProblem.Threefold.SpecialPeriods10
+import LeanPool.HopfProblem.Threefold.SpecialPeriods11
+import LeanPool.HopfProblem.Threefold.SpecialPeriods12
+import LeanPool.HopfProblem.Threefold.SpecialPeriods2
+import LeanPool.HopfProblem.Threefold.SpecialPeriods3
+import LeanPool.HopfProblem.Threefold.SpecialPeriods4
+import LeanPool.HopfProblem.Threefold.SpecialPeriods5
+import LeanPool.HopfProblem.Threefold.SpecialPeriods6
+import LeanPool.HopfProblem.Threefold.SpecialPeriods7
+import LeanPool.HopfProblem.Threefold.SpecialPeriods8
+import LeanPool.HopfProblem.Threefold.SpecialPeriods9
+import LeanPool.HopfProblem.Toric.CuspHoneycombHexagon
+import LeanPool.HopfProblem.Toric.DiagonalQuotient1
+import LeanPool.HopfProblem.Toric.DiagonalQuotient2
+import LeanPool.HopfProblem.Toric.DiagonalQuotient3
+import LeanPool.HopfProblem.Toric.DiagonalQuotient4
+import LeanPool.HopfProblem.Toric.ToricSpace1
+import LeanPool.HopfProblem.Toric.ToricSpace2
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology1
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology2
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology3
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology4
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology5
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology6
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology7
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology8
+import LeanPool.HopfProblem.TorusHomology.PeriodTorusHigherHomology9
+import LeanPool.HopfProblem.Uniformization.CuspUniformization1
+import LeanPool.HopfProblem.Uniformization.CuspUniformization2
+import LeanPool.HopfProblem.Uniformization.CuspUniformization3
+import LeanPool.HopfProblem.Uniformization.CuspUniformization4
+import LeanPool.HopfProblem.Uniformization.HolomorphicCousin
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods1
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods2
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods3
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods4
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods5
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods6
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods7
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods8
+import LeanPool.HopfProblem.Uniformization.SpecialPeriods9
+import LeanPool.HopfProblem.Uniformization.TriangleUniformizationGluing
 import LeanPool.Incompleteness
 import LeanPool.Incompleteness.Arith.D1
 import LeanPool.Incompleteness.Arith.D3

LeanPool/HopfProblem.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Boris Alexeev. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Boris Alexeev
+-/
+
+module
+
+public import LeanPool.HopfProblem.MainTheorem.Core3
+
+/-!
+# A complex structure on the six-sphere
+
+Source: url:https://github.com/plby/HopfProblem/tree/9ac8a456b526527837d7082ff775213ca8bc9809
+Authors: Boris Alexeev, Yury G. Kudryashov, Sebastian Kumar, The Formal Conjectures Authors
+Status: verified
+Main declarations: `Mathoverflow1973.mathoverflow_1973`
+Tags: complex-geometry, differential-topology, complex-manifolds, six-sphere, torus-fibrations
+MSC: 32Q55, 57R15
+-/
+
+/-!
+# A complex structure on the six-sphere
+
+This project formalizes the construction in Levent Alpöge's paper
+*A compact complex threefold fibred by tori over the projective line, and the six-sphere*.
+It constructs a compact complex threefold, proves that its underlying topological space is
+homeomorphic to the standard six-sphere, and transports the complex atlas to `unitSphere 6`.
+
+## Provenance
+
+The canonical source is Boris Alexeev's Apache-2.0-licensed
+[`plby/HopfProblem`](https://github.com/plby/HopfProblem) at commit
+`9ac8a456b526527837d7082ff775213ca8bc9809`. The thematic source tree was prepared in
+[upstream pull request #1](https://github.com/plby/HopfProblem/pull/1) at commit
+`bcbeff1324f22d228c9bde649532228826dab47d`. The original source states that most of its Lean
+code was written by Codex, so this import is classified as AI provenance.
+
+The mathematics follows [Alpöge's paper](https://alpo.ge/s6.pdf). The final statement was adapted
+from the Formal Conjectures rendering of MathOverflow question 1973. Complex-analysis material,
+including the Riemann mapping and Hurwitz developments, was adapted from Yury Kudryashov's
+[Mathlib pull request #33505](https://github.com/leanprover-community/mathlib4/pull/33505) at
+commit `d43061d911b1aeae0788591da437a3b115098962`. Topological material, including simple
+connectedness of spheres and path-factorization results used for van Kampen, was adapted from
+Sebastian Kumar's [Mathlib pull request #28246](https://github.com/leanprover-community/mathlib4/pull/28246)
+at commit `037ad801e1e5a5b7aa1750957c07f7769812effc`.
+
+The reused upstream material is Apache-2.0 licensed and was modified and reorganized here.
+Copyright (c) 2025, 2026 Yury Kudryashov; copyright (c) 2026 Sebastian Kumar; copyright 2025
+The Formal Conjectures Authors.
+-/