Repository navigation
Import the Hopf problem formalization - #392
Conversation
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 |
The visible analytic and C¹ declarations match their informal claims, but the partial diff elides the preserved headline and most of the construction, so faithfulness cannot be approved from this review. |
| Novelty | 🤔 discuss |
The visible headline declarations are not duplicates of Mathlib or any pooled project, but the heavily elided diff prevents an unconditional novelty pass. |
| Significance | 🤔 discuss |
The six-sphere complex-structure construction is a research-level, theory-building result worth pooling, but the elided diff prevents a pass verdict here. |
| Sources | ✅ pass |
The visible citation trail is internally consistent; the linked source commit and referenced paper cannot be independently verified from this partial diff, but nothing suspicious appears. |
| Code quality (advisory) | 🤔 discuss |
The visible portion is maintainable in places, but it contains an evidently dead private definition and widespread generated scope boilerplate; this review is based on a partial diff. |
| Aspect | Value |
|---|---|
| Proves the claim | ➖ unverifiable |
| Assumed, not proved | No explicit hypotheses appear in the two visible headline statements; hidden bundled assumptions or postulated structure cannot be audited because the relevant files are elided. |
| Already formalized | 🛑 EMPTY |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | complex geometry and differential topology |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: The visible exists_complex_analytic_atlas and exists_complex_atlas state exactly existence of a ChartedSpace on unitSphere 6 with IsManifold regularity ω and 1; the mathoverflow_1973 declaration and its dependency cone are elided.
This formalizes a major claimed construction addressing the famous Hopf problem by building a complex threefold and transporting its atlas to the six-sphere.
Code quality findings (3)
- dead-declaration —
LeanPool/HopfProblem/Foundations/Core5.lean:43
twistRelatorsis private and has no consumer in this module; because private declarations cannot serve as the project's API, it is dead code that should be removed (or used by a theorem in this file).
Evidence: private def twistRelators (a b d : ℤ) : Fin 5 → FreeGroup (Fin 3) :=
let c := FreeGroup.of (0 : Fin 3)
let x := FreeGroup.of (1 : Fin 3)
let y := FreeGroup.of (2 : Fin 3)
![c * x * (x * c)⁻¹, c * y * (y * c)⁻¹, x * y * (c ^ a)⁻¹, x ^ 3 * (c ^ b)⁻¹, y ^ 4 * (c ^ d)⁻¹] - import-residue —
LeanPool/HopfProblem/Foundations/Core1.lean:21
This module only definesLatticeMatrix, yet it opens a large unrelated collection of scopes (BigOperators,CategoryTheory,Convolution,UpperHalfPlane, etc.). The same blanketopen scopedblock is repeated across the imported files, making notation dependencies opaque and leaving generated residue that should be reduced to scopes actually used.
Evidence: 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
...
public
abbrev LatticeMatrix :=
Matrix (Fin 4) (Fin 4) ℤ
- import-residue —
LeanPool/HopfProblem/Foundations/Core5.lean:21
The blanket scope opening is also present in this small algebraic module, whose visible declarations use only integer arithmetic andFreeGroup; the unrelated topology, manifold, tensor, convolution, and uniformization scopes add maintenance noise. The repeated block should be removed or minimized per module.
Evidence: 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
...
def twistOrder (ℓ₀ ℓ₁ ℓ₂ : ℤ) : ℤ :=
12 * ℓ₀ - 4 * ℓ₁ - 3 * ℓ₂
Tokens: 1,474,743 in / 10,008 out across 5 rubric calls · Tier: codex-azure · Effort: xhigh · Billing: Codex account quota on Azure (no API credits)
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 |
|
Automated review update for the current head. I completed a bounded review of all changed modules and verified the repaired attribution card: Alexeev is credited for the source, Kudryashov and Kumar for Lean/mathlib contributions, and Formal Conjectures Authors for the formalization. No author-actionable attribution defect remains. |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
The whole-pool `runLinter` simpNF test of this private lemma now exceeds the 200000-heartbeat budget against the enlarged pool simp set; the lemma is only ever applied explicitly (rw / simp only), so it no longer needs the attribute. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Automated review — CI repair pushed; disposition needs-maintainer (unchanged)Reviewed exact head What broke. The required Repair. The lemma is applied only explicitly ( Why still needs-maintainer. The open decision is unchanged from 2026-09-04/09-08: whether this 260k-line, 34-minute-profile AI formalization of a complex structure on the six-sphere (Alexeev's source, Alpöge's construction) meets Lean Pool's significance and source bar. One consequence of the failure mode above is worth knowing when deciding: on every whole-pool |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
|
2026-09-18 exact-head reconciliation: Reviewed New at this head, and author-side: |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
|
End-of-cycle note (2026-09-18). The HopfProblem tree is unchanged through every auto-rebase sync today, so needs-maintainer stands for the source decision. On the announced repair attempt: a local build of the synced tree against |
The v4.34.0 bump merged into this branch (#436) broke the project; CI's Build pool failed in HomologyTheory/SingularMayerVietoris and stopped there. Building the whole project locally surfaced the rest. Nothing mathematical changes: every registered result still audits to propext, Classical.choice and Quot.sound. - Mathlib replaced the set-based `stdSimplex` by the bundled structure `Convexity.StdSimplex`, which `TopCat.toSSet` now uses. The singular chains here manipulate simplex coordinates as functions, so SingularMayerVietoris keeps a private copy of the retired set-based API (`SimplexSet`) and bridges to Mathlib's bundled simplices only at the `TopCat.toSSet` boundary (`toSimplex`/`ofSimplex`/`simplexIndexEquiv`); the face and chain-map compatibilities are now proved rather than `rfl`. The simplicial identity in TriangleRegularBaseFundamentalGroup is proved from `SimplexCategory.δ_comp_δ` instead of `SimplexCategory.toTop₀`. - `Filter.EventuallyEq.mfderiv_eq` now inserts a `tangentSpaceCast`; Smale1 adds a private cast-free `mfderiv_eq'` (the cast is definitionally the identity) and the Recognition files use it. - Renamed or reshaped Mathlib API: `logDeriv_mul`/`logDeriv_prod` (Pi forms), `IsOpenQuotientMap.secondCountableTopology`, `isClosed_of_discreteTopology`, `Finset.prod_le_prod₀`, removed `mul_le_one₀`, `JoinedIn.map` (ContinuousOn), `Set.equivOfEq`, `HasFDerivAt.isLittleO`, `ContinuousLinearMap.lipschitzWith`, `Sigma.ι_comp_desc`. - Linter fixes: `<;>` where sequencing suffices, an unused `rfl`, and the `[FiniteDimensional ℝ _]` instances the `unusedArguments` linter now reports along the general-position chains (Mathlib's `dense_compl_of_dimH_lt_finrank` no longer needs them). Validated: `lake build LeanPool.HopfProblem` warning-free (4546 jobs), `lake exe runLinter LeanPool.HopfProblem` (15 linters, 22275 declarations), whole-library `lint-style`, `mk_all --check`, the project card/declaration checks, the 216-declaration axiom audit and the compiled option audit. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Needs-maintainer cycle 2026-09-18: v4.34.0 port pushed, head
|
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent review and repair at 4c678f00e351762ae9243c4976542092ccf625ab: approve and merge after the refreshed protected checks pass.
The public endpoint is an unconditional complex-analytic ChartedSpace/IsManifold structure on Metric.sphere (0 : EuclideanSpace ℝ (Fin 7)) 1, using its standard subtype topology and Mathlib definitions. We traced the sphere aliases, actual compact complex threefold, recognition homeomorphism, atlas transport and complex-linear model change. A separate binding/instance audit found no substituted topology, weakened manifold predicate, shadow scalar type or hidden endpoint hypothesis. This is a substantial completed complex-geometry project, with a coherent construction and recognition development beyond existing Mathlib/pool headlines. Its large maintenance footprint is justified by that scope; code quality is 3/5, chiefly because the many numbered private modules make navigation expensive.
I corrected the entry prose and registry summary to say that the underlying topological space is homeomorphic to the sphere. The exposed recognition result does not assert compatibility with a preselected smooth atlas. This repair changes only prose: the Lean code tokens and every other registry value are unchanged, and the generated card remains current. git diff --check passes.
The former source-conflict hold is stale. The current Alpöge manuscript, opening discussion and section 10, explicitly challenges the non-normal-fibre reduction behind Campana–Demailly–Peternell, Corollary 2.3. Thus it acknowledges the conflict rather than silently quoting a different theorem. The pool card claims the atlas result directly formalized here; it does not claim a formal verification of that separate literature rebuttal. Pinned upstream and reused formalization credits remain explicit.
Full CI on the prior mathematical source passed compilation, linters and quality/trust gates. The source/instance inspection and proof-bridge review rely on those kernel checks; this is not a claimed line-by-line review of all 260k lines. The new prose-only head requires its own protected checks before landing. No remaining concrete semantic, source or significance blocker was found. COMMENT is used because the authenticated account authored the PR.
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:
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.