Import the Hopf problem formalization - #392
Conversation
|
Too many files changed for review (149 files, 100 file limit). Bypass the limit by tagging |
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 133,085 maxHeartbeats units across 147 files (260,324 added LOC). Sum of Count-heartbeats wall-clock total: 5293.94 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.HopfProblem.Recognition.Smale11 |
124.00 s |
LeanPool.HopfProblem.Recognition.Smale7 |
118.00 s |
LeanPool.HopfProblem.Recognition.Smale9 |
108.00 s |
LeanPool.HopfProblem.Recognition.Smale6 |
100.00 s |
LeanPool.HopfProblem.Recognition.Smale8 |
99.00 s |
LeanPool.HopfProblem.Hurewicz.ThirdHurewicz |
93.00 s |
LeanPool.HopfProblem.Recognition.Smale3 |
88.00 s |
LeanPool.HopfProblem.Recognition.Smale4 |
87.00 s |
LeanPool.HopfProblem.Recognition.Degree1 |
87.00 s |
LeanPool.HopfProblem.Recognition.Degree2 |
87.00 s |
LeanPool.HopfProblem.Recognition.Smale5 |
84.00 s |
LeanPool.HopfProblem.Recognition.Smale10 |
84.00 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 147 files; the per-file table shows only the 147 hottest by heartbeats. The full table and raw
lean --profileoutput for every file are in the run's step summary andproof-profileartifact.
Advisory only — never blocks merge.
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | 🤔 discuss |
On the partial diff, the two visible atlas theorems match their informals, but the preserved headline and decisive sphere-recognition inputs are elided, so faithfulness cannot be completed. |
| Novelty | ✅ pass |
Based on the partial diff, no Mathlib or pooled declaration already provides a complex ℂ³ manifold atlas on the standard six-sphere. |
| Significance | ✅ pass |
Based on the partial diff, this is a research-level theory-building project with a major named headline result. |
| Sources | ✅ pass |
Based on the partial diff, the exact upstream formalization and adapted Lean developments are credited consistently, though the external source contents are unverifiable here. |
| Code quality (advisory) | 🤔 discuss |
Based on the partial diff, the code is competent but carries pervasive split-generated boilerplate and duplicate infrastructure that a maintainer should inspect before merge. |
| Aspect | Value |
|---|---|
| Proves the claim | ➖ unverifiable |
| Assumed, not proved | The two visible headlines have no explicit hypotheses, but their witness uses a homeomorphism chosen from Smale.homeomorphic_sixSphere_of_homotopySixSphere applied to Degree.threefoldHomotopyEquiv; the defining patches for those inputs and the third headline are elided, so bundled or postulated content cannot be ruled out. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | complex geometry and differential topology |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: exists_complex_analytic_atlas and exists_complex_atlas existentially choose a ChartedSpace (EuclideanSpace ℂ (Fin 3)) (unitSphere 6) and prove IsManifold at orders ω and 1, respectively; the Lean statement of mathoverflow_1973 is not visible.
The project constructs a complex-analytic manifold atlas on the standard six-sphere, addressing the named Hopf problem through a substantial development of torus fibrations, homology, and manifold recognition.
Faithfulness findings (2)
- unverifiable-headline — PR-wide
Mathoverflow1973.mathoverflow_1973is registered as a headline, but its defining patch inLeanPool/HopfProblem/MainTheorem/Core3.leanis wholly elided. Its quantifiers, hypotheses, and conclusion cannot be checked against the informal without the declaration statement.
Evidence: prose only - unverifiable-assumed-content —
LeanPool/HopfProblem/Threefold/SixSphereComplexAtlas.lean:51
The final atlas construction depends on the sphere-recognition theorem andDegree.threefoldHomotopyEquiv, whose defining patches are not visible. The partial diff therefore does not permit checking whether the recognition content is proved rather than supplied through bundled fields.
Evidence: private def
SixSphereComplexAtlas.threefoldHomeomorph : SpecialPeriods.Threefold.Space ≃ₜ unitSphere 6 :=
Classical.choice
(Smale.homeomorphic_sixSphere_of_homotopySixSphere (ℂ × ComplexPlane₂)
SpecialPeriods.Threefold.Space SpecialPeriods.Threefold.real_dimension
Degree.threefoldHomotopyEquiv)
Code quality findings (2)
- agent-slop —
LeanPool/HopfProblem/Foundations/Core1.lean:19
The same catch-allopenandopen scopedblock is copied across nearly every visible module, including this file where the only declaration uses qualified names. This leaves each module dependent on a large ambient notation environment and obscures its actual dependencies. Prune these blocks per module rather than retaining monolithic-source boilerplate.
Evidence: open Set Function Filter Manifold Topology
open scoped BigOperators CategoryTheory Complex.UnitDisc ComplexConjugate ContDiff ContinuousMap
Convolution ENNReal EuclideanSpace Fin.NatCast InnerProductSpace Interval Matrix MatrixGroups
Modular NNReal Pointwise RealInnerProductSpace TensorProduct UniformConvergence Uniformity
UpperHalfPlane
/-- Integer matrices acting on the rank-four lattice used throughout the construction. -/
public
abbrev LatticeMatrix :=
Matrix (Fin 4) (Fin 4) ℤ
- duplicate-definition — PR-wide
Several infrastructure facts and constructions are maintained in parallel.ThreefoldHomologyStarCoproductdeclares the identical finite-biproduct witness twice; the generalizedElliptic.Equivariant.Datadevelopment repeats the specialized matrix and lift machinery fromElliptic.Core2; and the same local-compactness proof is declared under three names. Keep one exported witness for the exact duplicates, and move the generalized elliptic machinery before the specialized instance so the latter is defined through it.
Evidence: private theorem ThreefoldHomologyStarCoproduct.singularChainsFiniteBiproducts :
CategoryTheory.Limits.HasFiniteBiproducts (ChainComplex (ModuleCat.{0} ℤ) ℕ) :=
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
public
theorem ThreefoldHomologyStarCoproduct.homologyFiniteBiproducts :
CategoryTheory.Limits.HasFiniteBiproducts (ChainComplex (ModuleCat.{0} ℤ) ℕ) :=
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
private theorem Elliptic.familyPeriodEquiv_matrix (j : Kind) (z : SpecialPeriods.Disc)
(x : RealPlane₄) :
(familyPeriods j).periodEquiv z x =
((familyPeriods j).point z).val.matrix *ᵥ (fun i => (x i : ℂ)) := by
rw [HolomorphicPeriodMap.periodEquiv_coordinates]
ext i
fin_cases i <;> simp [PeriodPoint.matrix, Matrix.mulVec, dotProduct, Fin.sum_univ_four]
private theorem Elliptic.Equivariant.Data.periodEquiv_matrix {j : Elliptic.Kind}
(D : Elliptic.Equivariant.Data j) (z : SpecialPeriods.Disc) (x : RealPlane₄) :
D.periods.periodEquiv z x = (D.periods.point z).val.matrix *ᵥ (fun i => (x i : ℂ)) := by
rw [HolomorphicPeriodMap.periodEquiv_coordinates]
ext i
fin_cases i <;> simp [PeriodPoint.matrix, Matrix.mulVec, dotProduct, Fin.sum_univ_four]
private instance Elliptic.discLocallyCompact : LocallyCompactSpace SpecialPeriods.Disc :=
SpecialPeriods.unitDisc.isOpen.locallyCompactSpace
public
theorem
Elliptic.Equivariant.Data.discLocallyCompact : LocallyCompactSpace SpecialPeriods.Disc :=
SpecialPeriods.unitDisc.isOpen.locallyCompactSpace
private theorem Elliptic.LogGauge.discLocallyCompact : LocallyCompactSpace SpecialPeriods.Disc :=
SpecialPeriods.unitDisc.isOpen.locallyCompactSpace
Tokens: 2,703,739 in / 15,806 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $13.8743
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Vilin97
added
the
needs-maintainer
|
Automation disposition: needs-maintainer Reviewed exact head bc6e898. The Lean endpoint does construct a complex manifold structure on the real 6-sphere through the imported threefold/Smale chain, but this is a very recent claimed solution to a historically open problem, the card omits the underlying Alpöge paper and adapted contributors named upstream, Greptile could not review more than 100 files, and the 260k-line build/profile footprint is far beyond an automated repair. Source acceptance, attribution, and architecture require a maintainer decision. |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
|
Addressed the project-card attribution concern in 401d0fb:
The canonical repository attribution remains Boris Alexeev, so the source-repository authorship is not conflated with the underlying mathematics or adapted Lean components. Verification after the metadata change: |
|
Follow-up
Verification on the exact pushed source: full |
# Conflicts: # LeanPool/projects.yml
Automation disposition: needs-maintainerReviewed exact head |
1 participant
Summary
Imports Boris Alexeev's Apache-2.0-licensed formalization of a complex structure on the six-sphere as
LeanPool.HopfProblem.The preserved headline is:
Mathoverflow1973.mathoverflow_1973 : ∃ atlas, IsManifold 𝓘(ℂ, EuclideanSpace ℂ (Fin 3)) 1 (Mathoverflow1973.unitSphere 6)The project also exposes the stronger analytic result
Mathoverflow1973.SixSphereComplexAtlas.exists_complex_analytic_atlasand its differentiable corollary.Provenance
plby/HopfProblem@9ac8a456plby/HopfProblem#1@bcbeff13Both source revisions are recorded in the entry module. The canonical commit remains the project-card source; the split commit records the exact modular source tree imported here.
Integration and optimization
v4.34.0-rc1and the pool's current Mathlib.import Mathlib,import Mathlib.Tactic, or Selberg-sieve import. The final tactic shake reduced the focused Lake job closure from 4,673 to 4,497 (-3.8%)..ileanmetadataPeriodFamily/Core10material into its sole consumer, keeping the project at 147 modules after adding the pool entry/Prelude layout.simpNF, 125 initialunusedArguments, and 18 underscore-name findings; cascading unused arguments were also cleared).LeanPool.RiemannMappingTheorem/LeanPool.WhiteheadTheoremfor reuse. No statement-compatible replacement measurably reduced size or compile time without introducing fragile cross-project coupling, so none was retained.Measurements
The net source-size increase is the explicit privacy/public reflow, module and API documentation, and pool integration scaffolding required by the repository gates; the proof dependency cone itself lost the dead commands, unused binders, and redundant simp registrations above. The timed optimized full-source build preceded three final whitespace-warning fixes; a subsequent dependency-propagating project build and the final umbrella build were warning-free.
Verification
lake build LeanPool.HopfProblem— 4,673 jobs, warning-freelake exe runLinter LeanPool.HopfProblem— all 14 linters pass across 22,231 declarations plus 10,535 generated declarationslake exe lint-style LeanPool.HopfProblem— passeslake exe mk_all --check— passeslake build LeanPool— 9,882-job umbrella build passes, including collision checking against every existing pooled projectpropext,Classical.choice, andQuot.soundMathoverflow1973, apart from 37 intentional extensions inAnalyticOnNhd,Complex,PartialEquiv, andPath; the umbrella build confirms no collision with current LeanPoolThe repository-wide quality sweep was started against complete
LeanPool,Challenge, andSolutionenvironments, but was stopped after 12 minutes so CI can run that authoritative whole-repository audit. No failure had been reported; the project-targeted and static gates above are green.