Repository navigation
Import Sendov's conjecture and the Phelps–Rodriguez conjecture - #556
Conversation
Port of teorth/sendov at 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d (Apache-2.0, Lean source written by Claude Opus 5 under Terence Tao's direction) to Lean v4.35.0-rc3 and the module system: 69 upstream modules in the closure of Sendov.Conjecture plus a new kernel-checked Bernstein-certificate module. The 31 batch certificates and the large-degree endgame are checked by `decide +kernel` through list-polynomial identities instead of `ring` under raised heartbeat budgets; numerals beyond 90 digits are chunked; the Alpha17 bound uses explicit product hints. No set_option remains, and the clean project build drops from 1948 s to 226 s of CPU time. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
|
/review Please review the mathematics and source claims on head |
|
@greptileai please review this draft PR at |
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low risk] Adds mathematical proof library for polynomial conjectures. No new issue from the post-review changes prevents merging. SummaryThe PR imports the Sendov and Phelps–Rodriguez formalization, its supporting proofs and certificates, and the project registry and import entries. Since the previous review, the branch merged base-branch changes to generated metadata; the Sendov source and project card did not change. Reviews (6) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." |
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: 3,562,352 maxHeartbeats units across 70 valid files (16,850 added LOC). Sum of Count-heartbeats wall-clock total: 680.70 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with 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.Sendov.Reduction.Stat |
22.00 s |
LeanPool.Sendov.Reduction.Alpha17 |
21.00 s |
LeanPool.Sendov.LargeDegree.Monotone |
17.00 s |
LeanPool.Sendov.FiniteRange.Batch |
14.00 s |
LeanPool.Sendov.FiniteRange.Degree80To100 |
14.00 s |
LeanPool.Sendov.Reduction.BetaBound |
13.00 s |
LeanPool.Sendov.Reduction.Simplified |
12.00 s |
LeanPool.Sendov.Analytic.Polar |
11.00 s |
LeanPool.Sendov.Analytic.Origin |
11.00 s |
LeanPool.Sendov.Analytic.Jsum |
11.00 s |
LeanPool.Sendov.Analytic.OriginExact |
11.00 s |
LeanPool.Sendov.FiniteRange.Degree70To79 |
10.00 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 71 files; the per-file table shows only the 71 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.
…guez Bridge theorems from upstream Solution.lean, registered on the card. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
|
@greptileai please re-review at head |
Thorough review (REVIEW_RULES.md dimensions, plus engineering axes)Reviewed head Faithfulness — approve. Novelty — approve. No Sendov, Phelps–Rodriguez, Rubinstein, Maclaurin-inequality, or multiset AM–GM entry exists in the pool or in Mathlib ( Significance — approve. Sendov's conjecture was open from 1962; the full-generality proof is from 2026. The reusable layer is broader than the headline: Maclaurin/AM–GM for multisets, the defect inequality, the sharp Sources — approve. The card cites Tao's blog post (published 2026-08-12 23:10:54 UTC, inside the window), credits Lech Mazur's prior proof and formalization as upstream's README does, and attributes the boundary argument to Tang–Zhang arXiv:2508.10341 (5.1)/Remark 5.1 as upstream does. License Apache-2.0 verified in the upstream LICENSE; all file headers retained. Provenance Code quality — approve, advisory 4/5. The certificate redesign removes all 96
Engineering axes. CI on this head: module-system index check, full pool build with warning scan, challenge/solution build, Verdict: approve on content. Merge remains blocked by the repository-wide root-index capacity gate ( |
# Conflicts: # LeanPool/projects.yml
Changes requested by automated reviewReviewed exact head Blocking finding: generated Acceptance condition: land the separately reviewed central project-root index migration, rebase this PR, and pass all protected checks on the resulting exact head. Preserve generated-index correctness, repository quality checks, public declarations, and theorem statements. No mass source-module consolidation is requested of this PR for the legacy generated-root cap. Content approval does not clear the current gate failure; draft status is not its cause. This is changes requested, with no |
# Conflicts: # LeanPool.lean
There was a problem hiding this comment.
Independent integration verification — 2026-10-02, GPT-6.1-Sol/Ultra
PR #556 was merged by repository actor Vilin97 at 2026-10-02 19:11:53 UTC, from reviewed head cf9b8169d2a6112f546a89b96bc0f1a2e7be5232 to squash 4a4927fa3bc323dc9eb58c4287b7fa6ebf79cc7d. This review worker independently verified that result and did not execute the merge.
All 72 owned Lean files, the entry module and exact project card are identical to accepted source c1acd097dd462de31fca9edc80f5ef2071a98461; the mathematical, Apache licensing and first-party AI provenance verdicts carry forward. The generated project root has 71 sorted, distinct public imports, and the pool root adds its single Sendov project import. The same source tree and card are present in current main 710eb3b9b8d815bb00666a9a723c24d1896df675, whose final metadata commit changes only NOTICE and README.
Exact-head Lean Action CI 37048443229 completed SUCCESS: generated index, project/challenge builds, declaration lint, text style, repository quality, artifact retention and protected aggregate Build project passed. Documentation preflight and content separation also passed. Retained artifact 11246273192 is 26,114,805 bytes and unexpired through 2026-10-16T19:08:18Z; its manifest was independently matched to every exact-head source hash and all three toolchain/build inputs. There are no review threads or later substantive changes request.
Earlier draft, pending-CI and main-integration wording below is historical and superseded by this completed integration. No gate, waiver or mathematical source change was made by this review worker.
2026-10-02 current-status correction — substantive source approval carries forward. PR #556 is OPEN and ready for review at c800faa0d810858cb418ef6106a1126fe3187563 (isDraft: false). Its complete LeanPool/Sendov source tree, entry module, generated index, and project card are byte-identical to the accepted c1acd097dd462de31fca9edc80f5ef2071a98461 head. The previously verified AI proof provenance and mathematical source verdict remain supported. No source condition is newly opened.
Exact-head Lean Action CI 37024042868 completed successfully in rebase mode at this head. The generated index, combined Lean root, combined metadata validation, Check rebased root, and aggregate Build project passed. Previously validated modules were restored, so the full-validation fallback was skipped. All three required contexts pass. Retained rebase-project-build artifact 11234373631 is tied to this exact run/head and is unexpired through 2026-10-16T15:15:48Z.
The source is accepted for normal integration. This green run validates the existing head on base 0a29d01e8da977309a0aea5065ce0d1855a5da82; before integration, refresh against latest main and pass the protected checks for the resulting successor, then recheck threads and branch state. This existing COMMENTED review records the source verdict from the author account. Earlier draft and old-head status wording below is historical and superseded by this checkpoint.
2026-10-02 exact-head follow-up — substantive approval carries forward; protected checks passed. PR #556 is OPEN and draft at exact head 41b91c41e5429e194989917804d0ae2285a0de4b, integrated with main 0b41e3639c59e5788f6dfc0d5b40d5329c22ae0b. The complete LeanPool/Sendov source tree, entry module, and project card block are byte-identical to the approved c1acd097dd462de31fca9edc80f5ef2071a98461 head; the generated Imports.lean and single public root import remain present. The previously reviewed AI provenance matches the pinned upstream disclosure, and no new source or provenance finding is known.
Lean Action CI 37003752785 completed SUCCESS at this exact head in rebase mode: Plan, generated-index check, combined Lean root build, combined metadata validation, Check rebased root, and aggregate Build project passed. The full validation fallback was skipped because the prior validated project artifact was restored. Exact-head Documentation preflight and Content / non-content separation passed. Retained rebase-project-build artifact 11225362983 is unexpired through 2026-10-16T12:08:32Z.
The earlier capacity and pending-CI wording below is historical. The maintainer can mark the PR ready when the contributor intends to submit it. Canonical main has since advanced by a NOTICE/README metadata refresh to 9be87c9d66eea4341994be1b66b2f4940cc373fb; a later merge needs the normal live main/head check and protected checks on any successor. This COMMENTED review records a source verdict from the author account, not formal self-approval.
Historical source review and status follow.
Reviewed exact draft head c1acd097dd462de31fca9edc80f5ef2071a98461: substantive content approved; integration and required CI pending.
All 71 Sendov source modules and the project card remain byte-identical to the comprehensive mathematical review. The full Sendov and Phelps–Rodriguez statements, including the equality case, remain faithful to the pinned upstream source, significant, and distinct from existing pool content. The Apache license, recorded AI proof provenance, and kernel-checked certificate approach are preserved. The migration adds a generated LeanPool.Sendov.Imports file with exactly 71 sorted, distinct public imports and one aggregate-root import; the former generated-root capacity objection is resolved by the separately merged project-root migration. This PR changes no check, limit, or waiver.
The previous changes request concerned only that former capacity gate. Exact-head sharded CI is still running, and this head is behind current main ec381e198b00513a1a56871b5de16edcb38da03d. Keep it draft until the completed source run is inspected, current main is integrated losslessly, and Build project, content separation, and documentation preflight all pass on the resulting exact head. Recheck review threads and branch state before a normal protected merge.
This account authored the PR, so COMMENTED records the source verdict.
…ndov-main-ec381-review-20261001
|
Reviewed exact head The integration merge preserves every Sendov mathematical source file, the project card, the complete generated The substantive source review carries forward. This draft remains pending exact-head protected CI; no Build project result or merge approval is claimed yet. The former aggregate-root size request is superseded by the shipped project-root index. |
# Conflicts: # LeanPool/projects.yml
Approved for protected mergeReviewed exact head The full local 3,064-job build, declaration/style linters, 72-file/735-declaration axiom/option audit and index check pass. Exact-head protected Build project, Content / non-content separation and Documentation preflight are green, GitHub is CLEAN, and no unresolved conversation or human change request remains. The author marked the PR ready during this cycle. Normal protected squash merging is now justified. Formal self-approval is unavailable to the PR-author account. |
# 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
|
/review Fresh exact-head review requested at |
1 participant
Independent integration verification — 2026-10-02, GPT-6.1-Sol/Ultra
PR #556 was merged by repository actor
Vilin97at 2026-10-02 19:11:53 UTC, from reviewed headcf9b8169d2a6112f546a89b96bc0f1a2e7be5232to squash4a4927fa3bc323dc9eb58c4287b7fa6ebf79cc7d. This review worker independently verified that result and did not execute the merge.All 72 owned Lean files, the entry module and exact project card are identical to accepted source
c1acd097dd462de31fca9edc80f5ef2071a98461; the mathematical, Apache licensing and first-party AI provenance verdicts carry forward. The generated project root has 71 sorted, distinct public imports, and the pool root adds its single Sendov project import. The same source tree and card are present in current main710eb3b9b8d815bb00666a9a723c24d1896df675, whose final metadata commit changes only NOTICE and README.Exact-head Lean Action CI 37048443229 completed SUCCESS: generated index, project/challenge builds, declaration lint, text style, repository quality, artifact retention and protected aggregate Build project passed. Documentation preflight and content separation also passed. Retained artifact
11246273192is 26,114,805 bytes and unexpired through 2026-10-16T19:08:18Z; its manifest was independently matched to every exact-head source hash and all three toolchain/build inputs. There are no review threads or later substantive changes request.Earlier draft, pending-CI and main-integration wording below is historical and superseded by this completed integration. No gate, waiver or mathematical source change was made by this review worker.
2026-10-02 current-status correction — substantive source approval carries forward. PR #556 is OPEN and ready for review at
c800faa0d810858cb418ef6106a1126fe3187563(isDraft: false). Its completeLeanPool/Sendovsource tree, entry module, generated index, and project card are byte-identical to the acceptedc1acd097dd462de31fca9edc80f5ef2071a98461head. The previously verified AI proof provenance and mathematical source verdict remain supported. No source condition is newly opened.Exact-head Lean Action CI 37024042868 completed successfully in rebase mode at this head. The generated index, combined Lean root, combined metadata validation, Check rebased root, and aggregate Build project passed. Previously validated modules were restored, so the full-validation fallback was skipped. All three required contexts pass. Retained
rebase-project-buildartifact11234373631is tied to this exact run/head and is unexpired through 2026-10-16T15:15:48Z.The source is accepted for normal integration. This green run validates the existing head on base
0a29d01e8da977309a0aea5065ce0d1855a5da82; before integration, refresh against latestmainand pass the protected checks for the resulting successor, then recheck threads and branch state. This existing COMMENTED review records the source verdict from the author account. Earlier draft and old-head status wording below is historical and superseded by this checkpoint.Historical acquisition description
Imports Terence Tao's Lean formalization of Sendov's conjecture and the Phelps–Rodriguez conjecture in full generality, following Tao's digestion of Lech Mazur's proof, together with its reusable infrastructure: the top case of Maclaurin's inequality and multiset AM–GM (
Multiset.esymm_card_pred_le,Multiset.prod_le_mean_pow), the defect inequality on the closed unit disk, a sharp bound onlog (sinh h / h), a packed-exponentiation bridge for exact moment integrals, and a new kernel-checked Bernstein-certificate module.Draft: exact-head CI pending. The separately merged project-root migration (#558 and #559) resolved the former
LeanPool.leancapacity blocker. This PR now addsLeanPool/Sendov/Imports.lean, a generated project-root index with 71 unique, sortedpublic importlines covering every Sendov source module, and adds its one import toLeanPool.lean. The reviewed source and project card are preserved. Lean Action CI for heade648cfb78is still running; currentmainis integrated ate648cfb78; keep the PR draft until the required checks pass on this exact head. This PR changes no gate, generator, workflow, linter setting, waiver, or unrelated project.Significance and dates
n ≥ 2polynomial with all zeros in the closed unit disk has a critical point within distance 1. The Phelps–Rodriguez strengthening makes the distance strict unless the zero lies on the unit circle andp = c (zⁿ − aⁿ); the boundary case recovers Rubinstein's theorem (Sendov.rubinstein_one).Upstream, license, provenance
1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d(public). LICENSE is Apache-2.0; every file carries Tao's copyright header, retained verbatim.AI: the upstream README states that essentially all Lean source was written by Claude Opus 5 in Claude Code under Tao's direction and review, with Tao supplying the informal proof, staged plans, and mathematical decisions. Recorded in the card'sprovenance_note.Scope
69 of the 76 upstream modules: exactly the dependency closure of
Sendov.Conjecture, plus the entry module and the newFiniteRange/Certificate.lean(71 modules, 16,850 lines). Not imported: six development cross-check modules (Degree6,Degree8,Degree20,Degree20Packed,Degree53Packed,Degree97Packed) andReduce.lean, none of which the main theorems depend on. The upstreamChallenge/Solutioncomparator pair restates the same two theorems and was not duplicated.Porting changes
public import,@[expose] public section);Mathlib.Basic.Real.Basicand explicit tactic imports where module-system Mathlib files no longer re-export them.ringidentity for a degree-up-to-78 Bernstein expansion and afield_simp; ringdenominator clearing, each undermaxHeartbeats 2000000andmaxRecDepth 4000000, withlinter.style.longLinedisabled around numerals of up to 29,000 digits; the degree-58 endgame certificate usedmaxHeartbeats 4000000. The newSendov.FiniteRange.Certificatemodule defines list-polynomial powers, Bernstein expansion (Sendov.bern), the batch numeratorSendov.batchP n₀ n₁ k L Nmom, and proves once, for symbolicn₀ n₁ k, that positivity ofbatchPgives the batch bound (Sendov.batch_lt_one) and that positive Bernstein coefficients give positivity (Sendov.pev_pos_of_bern). Each batch now supplies its data (Lc,betac,tauc,Nmomc,Bc) and discharges every closed computation withdecide +kernel; numerals over 90 digits are assembled from decimal chunks bySendov.big. The Bernstein coefficients are those of upstream scaled by the integer factor between upstream's cancelled numerator andbatchP; a Python cross-check reproduced every upstream numerator and certificate exactly before the Lean files were generated. The endgame (LargeDegree/Endgame.lean) uses the same infrastructure, with(3+α)^48andγ⁴generalized before clearing denominators so nothing of degree 48 is expanded.Reduction/Alpha17.lean: the fournlinarithcalls that neededmaxHeartbeats 1000000are closed from one explicit product hint each (nlinarith only [...]).Batch50To51,Degree50To51) for Mathlib's naming linters; docstrings added to the generated constants; one box-drawing glyph in a comment diagram replaced.set_optionoverrides are gone; nonolint, nomaxHeartbeats, nomaxRecDepth, no linter disables remain.Trust and axiom audit
#print axiomsover all 733 enumerated declarations of the imported modules: onlypropext,Classical.choice,Quot.sound. The pool's compiled-environment option/backdoor audit overLeanPool.Sendovreports no finding.sorry,axiom,native_decide,unsafe,partial,opaque,#eval, or floating point;decide +kernelis kernel reduction and introduces noofReduceBool.Historical local checks (worktree on pre-migration base
220627f7d6, Mathlib v4.35.0-rc3)lake build LeanPool.Sendov(clean project artifacts)lake exe runLinter LeanPool.Sendovlake exe lint-style LeanPoollake exe mk_all --module --checkquality --static-onlyLeanPool.lean:1); the project-root migration supersedes this result#print axioms+ option-backdoor audit (quality internals)These local results predate the project-root migration. The current exact-head Lean Action CI run is pending; its assembled build, index check, linters, and repository quality check will establish the current result.
Compile-time measurements
Same 16-vCPU shared VM, warm Mathlib oleans, project artifacts deleted before each run,
/usr/bin/time -v lake build LeanPool.Sendov; other jobs were active, so numbers are observed, not isolated.Per-module wall times inside the parallel clean builds, before → after:
Degree80_100362 s →Degree80To10021 s;Degree70_79311 s → 18 s;Degree64_69289 s → 16 s; the 31 batch files 3,916 s → 305 s in total (built alone,Degree80To100takes 3.6 s);Endgame112 s → 6.5 s;Alpha1750 s → 9.6 s; the newCertificatemodule 2.2 s. The remaining time is ordinary analytic elaboration (Monotone19 s,Simplified12 s,Stat10 s); no further material safe shortcut is evident without changing statements.🤖 Generated with Claude Code