Repository navigation
Integrate eight reviewed formalization projects - #467
Merged
Merged
Conversation
# 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
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>
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
Two independent proofs of Euler's pentagonal number theorem, sharing no lemmas: a combinatorial route via Franklin's sign-reversing involution, and a q-series route through q-Pochhammer symbols, Euler's identities and the Cauchy identity to the Jacobi triple product, both as a formal power series identity over an arbitrary commutative ring and analytically over the complex numbers. Overlap with existing work is declared in the project card rather than left to be discovered. The Franklin route and the analytic pentagonal number theorem overlap the pooled `pentagonal-number-theorem` entry, whose analytic form is stated over RCLike fields and is the more general of the two. The q-Pochhammer and Gaussian binomial definitions and Euler's two identities overlap arXiv:2607.01544, where the latter appear as qPochhammerInf_eq_tsum and qPochhammerInf_neg_eq_tsum. The distinct contribution is the complex-analytic layer: the Jacobi triple product over ℂ for ‖q‖ < 1, ‖z‖ < 1, z ≠ 0 with an extension to the punctured disc, the analytic Cauchy identity, and the summability and locally-uniform-convergence machinery these require. The arXiv:2607.01544 development is non-archimedean throughout and mentions Complex in no file; ℂ is not a NonarchimedeanRing, so those results do not specialize to it. The pooled pentagonal entry has no Jacobi triple product. provenance: AI. The Lean proofs in both routes were largely generated by Aristotle (Harmonic). The Franklin route follows a blueprint written by the authors, lemma by lemma, and carries substantially more manual intervention and review; the q-series route is machine-generated blueprint and all, with the authors restructuring the library, renaming its API and reviewing statements. Builds warning-free against the pool's Mathlib; no sorry, no axioms beyond propext / Classical.choice / Quot.sound, no unsafe or partial. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
P1 Formal JTP is monomorphic — correct. `FPS.lean` has `local notation "A" => LaurentPolynomial ℂ`, so `jacobiProd : A⟦X⟧` is fixed to (LaurentPolynomial ℂ)⟦X⟧ and the theorem takes no coefficient-ring parameter. The "arbitrary commutative ring" wording was wrong in both the main_results entry and the project summary; both now state the actual setting. The claim is narrowed rather than the development generalized, since generalizing is real work and should not ride along in a metadata fix. P1 Source revision missing — added `source.revision`, pinning the upstream commit the vendored copy was taken from. P2 Broad Mathlib imports — CODE_QUALITY.md forbids them outright, so this is treated as blocking. All four Franklin files replaced `import Mathlib` with the specific modules they use. Two corrections were needed along the way: `Mathlib.Tactic.Omega` no longer exists (omega is in Lean core), and `FormalPowerSeries.lean` additionally needs `Mathlib.Tactic.LinearCombination` and `Mathlib.Tactic.Zify`, which the blanket import had been supplying silently. No broad import remains anywhere in the project. P2 Module documentation is stale — correct on both counts. Franklin/Lemmas.lean listed five names under "Main results" that are not declared anywhere; it now names the DP*/pe_minus_po_* declarations that exist. FPS_Euler.lean claimed to prove euler_second_identity, which is proved downstream in FPS_Algebra.lean; its docstring now describes the unit and factorisation lemmas the module actually contains and says where the identity is proved. Still builds warning-free: 0 errors, 0 warnings. The three remaining P2 findings are not addressed here and are answered on the PR: the duplicated JTP assembly and the JTP_Helpers dead branch are real observations about proof structure, and the namespace question affects the upstream project's public API rather than the vendored copy. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Vilin97
commented
Sep 21, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
Author
There was a problem hiding this comment.
Integration review at e3534f082da59a0f43c32166f7f2adb2753e8e03: approve, subject to the required checks on this combined head.
I independently reconstructed the union from the eight reviewed PR heads. All 303 project source files match their accepted revisions byte-for-byte; every existing registry card is unchanged and the eight added cards exactly match the accepted cards. The generated index is exactly the sorted inventory, with its original header preserved. The diff touches only those sources, the registry and the index; all eight source heads are ancestors, and git diff --check passes. A second independent union audit reached the same result.
The substantive project reviews are linked in the description. The Hopf wording repair is included; there are no further source edits introduced by integration. The combined build/lint/quality checks will validate the projects together. Once those checks pass and the base and review threads remain clear, use an ordinary protected merge commit, preserving the source PR histories. No administrator override or configuration change is authorized by this review.
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.  No concrete correctness, integration, provenance, or maintainability defect was identified in the combined contribution. SummaryThis PR integrates eight previously reviewed formalization projects into the shared Lean Pool tree and updates the aggregate module index and project catalog.
Reviews (1) · Last reviewed commit: "Merge reviewed PR #392 into integration ..." |
Contributor
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: 193,136 maxHeartbeats units across 303 files (318,298 added LOC). Sum of Count-heartbeats wall-clock total: 3576.60 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.Smale1 |
65.00 s |
LeanPool.HopfProblem.Recognition.Smale11 |
61.00 s |
LeanPool.HopfProblem.Recognition.Smale7 |
60.00 s |
LeanPool.HopfProblem.Recognition.Smale9 |
58.00 s |
LeanPool.HopfProblem.Recognition.Smale6 |
57.00 s |
LeanPool.HopfProblem.Recognition.Smale8 |
53.00 s |
LeanPool.HopfProblem.Recognition.Degree2 |
52.00 s |
LeanPool.HopfProblem.Recognition.Degree1 |
49.00 s |
LeanPool.HopfProblem.Recognition.Smale4 |
47.00 s |
LeanPool.HopfProblem.Hurewicz.ThirdHurewicz |
47.00 s |
LeanPool.HopfProblem.Recognition.Smale5 |
44.00 s |
LeanPool.HopfProblem.Recognition.Smale10 |
44.00 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 303 files; the per-file table shows only the 303 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.
This was referenced Sep 21, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This integrates eight independently reviewed formalization projects through one combined-tree validation. Each original PR head is preserved as a merge parent, so a merge commit for this PR preserves every contribution and lets GitHub mark the source PRs merged by ancestry.
The included projects and their public reviews are:
All project source files and their eight registry cards were compared against the accepted review revisions. The combined diff is exactly their union: 303 Lean files, the project registry, and the generated module index. Registry conflicts were resolved with the repository’s existing card-preserving merger; the index was regenerated. Every source head is an ancestor of the integration commit.
git diff --checkpasses. Gates, workflows, dependencies and non-content files are unchanged.Required CI and the independent integration review must pass on the combined tree before landing. Individual successful CI results remain linked from the project reviews. Merge this PR using a merge commit, preserving the original PR histories.