Repository navigation
Import the Aaronson–Ambainis influence conjecture formalization - #778
Conversation
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Separate thorough review of 18a27d4b6faeb3759282569ce73dfc9642279d2a: approve for content, with no unresolved findings. Required CI and configured reviews remain pending, so the PR is not ready for queue entry yet.
{
"review_type": "Acquisition agent's separate thorough review pass",
"reviewed_commit": "18a27d4b6faeb3759282569ce73dfc9642279d2a",
"conclusion": "approve",
"merge_readiness": "Required CI and configured GPT/Greptile review completion are still pending; this content assessment does not authorize bypassing them.",
"coverage": {
"complete_diff": true,
"files": 85,
"mathematical_upstream_modules": 82,
"method": "Inspected all upstream mathematical source in 15 bounded chunks, separately re-read initially elided portions, checked all five card result declarations and proof dependency closure, and reviewed each port/optimization change against the preserved baseline. Read the live shared rules and all five rubrics."
},
"faithfulness": {
"verdict": "pass",
"evidence": "AaronsonAmbainis.PrintedConjecture quantifies over arbitrary N,d and MvPolynomial (Fin N) R, total degree at most d, pointwise [0,1] bounds, and positive epsilon below uniform variance. Its conclusion uses the uniform squared bit-flip difference, without the sign-cube factor 1/4, and lower bound (epsilon/d)^7. The unconditional Main endpoints are closed through Chain and Bridge.Capstone; the Row/Pack/Dual chain constructs the needed fractional rows rather than assuming their existence.",
"boundaries": "Positive variance rules out the zero-variable and degree-zero cases; the bridge proves the necessary positivity before division. Positivity.lean and Row.HypothesisCheck supply nontrivial witnesses and a counterexample showing why the block parameter must be positive.",
"assumptions": "Only the fourth, stronger constant endpoint has FbsDegreeBound as an input. The card explicitly discloses that condition. The three main declarations are unconditional closed propositions. Quantum simulation consequences are explicitly excluded."
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"evidence": "Searched the current pool cards, sources and history; open/closed PRs and issues; exact pinned Mathlib and TauCeti source; and public GitHub code/PR searches. Read the closest pool BlockSpectralSensitivity theorem: it concerns block versus spectral sensitivity and is a different result. Read the TauCeti symplectic determinant lexical hit: unrelated. No equivalent main endpoint was found. This is bounded corpus evidence, not an assertion that lexical search exhausts all prior art."
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"mode": "theory_building",
"evidence": "Closes a named bounded-polynomial influence conjecture from quantum query complexity, with explicit constants. The finite-cube transformations, degree calculus, determinant pairings, fractional certificates, packing/cover duality, all-pairs bounds and averaging lemmas are reusable beyond the endpoint. The imported source is structured mathematical proof rather than generated case-table or certificate bulk."
},
"sources_and_license": {
"verdict": "pass",
"source_match": "matches",
"evidence": "Verified public release commit 2a6ceaef872ae993708950f951989134084b851a and the November 6 PSI announcement inside the exact acquisition window. Read LICENSE and NOTICE: Apache-2.0 code/documentation, AI proof provenance, David Turturean attribution. Compared the original Aaronson-Ambainis Conjecture 6, the upstream paper's Theorem 1.1 and Corollary 1.2 constants, and Agarwal-Ben-David arXiv:2410.19062v2 Theorem 1.7 against the formal propositions. Relevant NOTICE attribution is retained; upstream-only paper and tooling are excluded. Corrected stale local-paper references in three imported comments."
},
"engineering": {
"verdict": "pass",
"code_quality": 3,
"evidence": "Coherent dependency closure with 82 mathematical modules, complete generated Imports and one card. Namespaced public API and pinned dependencies. Replaced five broad Mathlib imports, consolidated eight duplicate degree-calculus proofs, updated coefficient APIs/deprecated names, removed diagnostics and redundant tactics/instance hypotheses, fixed styles. No proof weakening, waiver, forbidden option or gate modification. Variable-degree product generality is preserved.",
"trust": "Warning-as-error build passes. Production declaration linters pass for 84 modules and 738 declarations. Production compiled axiom and option-backdoor audits cover all 84 modules and report zero findings. Generated card declarations and card sync pass; static repository quality, style and generated indexes pass.",
"performance": "Comparable fresh project builds with cached exact dependencies and LEAN_NUM_THREADS=4: 124.24s -> 55.94s wall, peak RSS 3064708 -> 1512696 KB; 84 modules in each. Per-file timings and synchronous command-heartbeat profiles inspected. Shared-VM timings have normal scheduling variance. No remaining material safe optimization was evident.",
"maintenance": "Ordinary proof scripts and small topical modules, no vendored toolchain, external runtime, generated table burden or extra package dependency. All changes are content-only; fixed LeanPool.lean and independent user work are preserved."
},
"ci_observed": "Final-head local checks pass; GitHub validation workflows have started. Applicable required contexts are assessed individually, and daily documentation publishing is excluded from merge readiness.",
"findings": []
}
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] No blocking code issue was found, but external source checks remain unverified. SummaryImports the Aaronson–Ambainis proof and supporting finite-cube infrastructure. The latest change narrows the project card’s claims about packing-cover duality.
Reviews (4) · Last reviewed commit: "Keep influence results as headlines and ..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Final-head thorough review of 29a1ba2684fc4b87fb063543db25e60a12103cbd: approve, with no unresolved findings. This updates the earlier review after the Greptile cleanup and scoped-import follow-up. Required CI and the configured GPT review must still pass before native-queue entry.
{
"review_type": "Acquisition agent's separate thorough review pass",
"reviewed_commit": "29a1ba2684fc4b87fb063543db25e60a12103cbd",
"conclusion": "approve",
"merge_readiness": "Required CI and configured GPT/Greptile review completion are still pending; this content assessment does not authorize bypassing them.",
"coverage": {
"complete_diff": true,
"files": 85,
"mathematical_upstream_modules": 82,
"method": "Inspected all upstream mathematical source in 15 bounded chunks, separately re-read initially elided portions, checked all five card result declarations and proof dependency closure, and reviewed each port/optimization change against the preserved baseline. Read the live shared rules and all five rubrics. Final follow-up commits were fully inspected and rebuilt; no mathematical statement changed."
},
"faithfulness": {
"verdict": "pass",
"evidence": "AaronsonAmbainis.PrintedConjecture quantifies over arbitrary N,d and MvPolynomial (Fin N) R, total degree at most d, pointwise [0,1] bounds, and positive epsilon below uniform variance. Its conclusion uses the uniform squared bit-flip difference, without the sign-cube factor 1/4, and lower bound (epsilon/d)^7. The unconditional Main endpoints are closed through Chain and Bridge.Capstone; the Row/Pack/Dual chain constructs the needed fractional rows rather than assuming their existence.",
"boundaries": "Positive variance rules out the zero-variable and degree-zero cases; the bridge proves the necessary positivity before division. Positivity.lean and Row.HypothesisCheck supply nontrivial witnesses and a counterexample showing why the block parameter must be positive.",
"assumptions": "Only the fourth, stronger constant endpoint has FbsDegreeBound as an input. The card explicitly discloses that condition. The three main declarations are unconditional closed propositions. Quantum simulation consequences are explicitly excluded."
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"evidence": "Searched the current pool cards, sources and history; open/closed PRs and issues; exact pinned Mathlib and TauCeti source; and public GitHub code/PR searches. Read the closest pool BlockSpectralSensitivity theorem: it concerns block versus spectral sensitivity and is a different result. Read the TauCeti symplectic determinant lexical hit: unrelated. No equivalent main endpoint was found. This is bounded corpus evidence, not an assertion that lexical search exhausts all prior art."
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"mode": "theory_building",
"evidence": "Closes a named bounded-polynomial influence conjecture from quantum query complexity, with explicit constants. The finite-cube transformations, degree calculus, determinant pairings, fractional certificates, packing/cover duality, all-pairs bounds and averaging lemmas are reusable beyond the endpoint. The imported source is structured mathematical proof rather than generated case-table or certificate bulk."
},
"sources_and_license": {
"verdict": "pass",
"source_match": "matches",
"evidence": "Verified public release commit 2a6ceaef872ae993708950f951989134084b851a and the November 6 PSI announcement inside the exact acquisition window. Read LICENSE and NOTICE: Apache-2.0 code/documentation, AI proof provenance, David Turturean attribution. Compared the original Aaronson-Ambainis Conjecture 6, the upstream paper's Theorem 1.1 and Corollary 1.2 constants, and Agarwal-Ben-David arXiv:2410.19062v2 Theorem 1.7 against the formal propositions. Relevant NOTICE attribution is retained; upstream-only paper and tooling are excluded. Corrected stale local-paper references in three imported comments."
},
"engineering": {
"verdict": "pass",
"code_quality": 3,
"evidence": "Coherent dependency closure with 82 mathematical modules, complete generated Imports and one card. Namespaced public API and pinned dependencies. Replaced five broad Mathlib imports, consolidated eight duplicate degree-calculus proofs, updated coefficient APIs/deprecated names, removed diagnostics and redundant tactics/instance hypotheses, fixed styles. No proof weakening, waiver, forbidden option or gate modification. Variable-degree product generality is preserved. Greptile\u2019s three repeated-proof groups are consolidated in common modules, with public namespace aliases preserved; the resolved thread records the fix.",
"trust": "Warning-as-error build passes. Production declaration linters pass for 84 modules and 738 declarations. Production compiled axiom and option-backdoor audits cover all 84 modules and report zero findings. Generated card declarations and card sync pass; static repository quality, style and generated indexes pass.",
"performance": "Comparable fresh project builds with cached exact dependencies and LEAN_NUM_THREADS=4: baseline 124.24s wall / 256.60s user / 3064708 KB peak RSS; final 81.65s / 130.68s / 1525272 KB (34.3% wall, 49.1% user-CPU reduction); 84 modules each. An earlier optimized run took 55.94s. Per-file timings and synchronous command-heartbeat profiles inspected. Shared-VM scheduling variance affects wall times. No remaining material safe optimization was evident.",
"maintenance": "Ordinary proof scripts and small topical modules, no vendored toolchain, external runtime, generated table burden or extra package dependency. All changes are content-only; fixed LeanPool.lean and independent user work are preserved."
},
"ci_observed": "Final-head local checks pass; GitHub validation workflows have started. Applicable required contexts are assessed individually, and daily documentation publishing is excluded from merge readiness.",
"findings": []
}
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: 877,314 maxHeartbeats units across 84 valid files (10,417 added LOC). Sum of Count-heartbeats wall-clock total: 297.12 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.AaronsonAmbainis.Level.Integral |
5.90 s |
LeanPool.AaronsonAmbainis.TwoSided.CauchySchwarz |
4.60 s |
LeanPool.AaronsonAmbainis.Level.ThirdMoment |
4.60 s |
LeanPool.AaronsonAmbainis.Level.Increments |
4.30 s |
LeanPool.AaronsonAmbainis.Bridge.PrintedAA |
4.10 s |
LeanPool.AaronsonAmbainis.Defs |
3.90 s |
LeanPool.AaronsonAmbainis.Average.Influence |
3.40 s |
LeanPool.AaronsonAmbainis.Level.Integrated |
3.20 s |
LeanPool.AaronsonAmbainis.Level.Median |
3.00 s |
LeanPool.AaronsonAmbainis.Average.Coordinate |
3.00 s |
LeanPool.AaronsonAmbainis.Pack.Packing |
2.90 s |
LeanPool.AaronsonAmbainis.Bridge.PrintedRow |
2.90 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 84 files; the per-file table shows only the 84 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.
|
/review |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent whole-project source review at 29a1ba2684fc4b87fb063543db25e60a12103cbd: favorable for significance, faithful statements, nonvacuity, completeness, and code quality. The review covers all 84 current Lean modules (10,417 lines), with separate mathematical lanes for the determinant/level-set/averaging development, Markov/packing/duality construction, and headline normalization bridges.
The Mathlib-only Conjecture.lean states the actual bounded real-polynomial influence problem. The three unconditional endpoints close the proof chain through proved determinant, row, packing and finite-duality results. The ordinary squared-flip influence on the 0/1 cube, the squared half-difference influence on the sign cube, and their explicit constants agree with the cited statements. Positive variance supplies the needed degree and coordinate positivity; concrete coordinate-polynomial examples establish nonvacuity. The stronger fourth endpoint retains its explicit FbsDegreeBound hypothesis.
The import has substantial reusable mathematical content. Fixed upstream 2a6ceaef872ae993708950f951989134084b851a, its license/NOTICE and primary sources support the Apache-2.0 attribution and AI provenance. The separately copyrighted paper is excluded. Inspection of the pinned libraries, current pool candidates and relevant current Tau Ceti candidates found no duplicate headline theorem; existing sensitivity, Boolean correlation and Fourier results have different premises or conclusions. This is a bounded source comparison, not a claim that every supporting lemma is new. The former cube/character/minimal-monomial duplication is now handled by shared providers and forwarding lemmas. No material source change is requested.
This completes the separate thorough source review. The current PR's configured GPT/Greptile requirement and applicable protected CI still need to be satisfied before normal queue admission. Author-reported local builds, artifact comparisons and performance measurements are not adopted as independent validation here.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Validation addendum for the thorough review of 29a1ba2684fc4b87fb063543db25e60a12103cbd: approve, no unresolved author-actionable findings.
Lean Action CI passed the project build, declaration linters, style, and repository quality/trust checks. All eight protected contexts completed successfully or were skipped by their applicable path filters. No aggregate status rollup or daily documentation publisher was used for this decision.
Proof profiling succeeded on retry after an Elan-download HTTP 504: 84 valid files, zero errors, 81.34s changed-module build, 877,314 heartbeat units. Local comparable clean builds measured 124.24s baseline and 81.65s final (an earlier optimized run measured 55.94s on this shared VM).
Greptile reviewed this final head with no blocking code finding; its duplicate-proof finding was repaired and resolved. The configured GPT review was requested after CI success and has not yet published a verdict. The PR remains open with auto-merge disabled pending that external result; no native-queue entry is authorized before it approves.
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All four card headlines match the Lean statements, including the disclosed condition for the sharper constant. |
| Novelty | ✅ pass |
No duplicate of the four influence headlines was found in pinned Mathlib or the inspected pool results; the broader Tau Ceti comparison remains unverifiable from the supplied candidates. |
| Significance | ✅ pass |
The Aaronson–Ambainis influence bounds and substantial supporting theory meet the pool’s research-level significance bar. |
| Sources | ✅ pass |
The pinned upstream paper supports the stated bounds, normalizations and conditional refinement; the upstream formalization and mathematical predecessors are explicitly credited. |
| Code quality (advisory) | ✅ pass |
The complete diff is competently organized into reusable proof layers, with no material maintenance issue found. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The stated degree, cube range and positive variance lower bound are hypotheses; only the improved constant additionally assumes FbsDegreeBound, as disclosed in the card. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | analysis of Boolean functions |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The Lean proves the stated influence bounds with the claimed quantifiers, constants and normalizations; positive variance excludes zero degree and an empty coordinate set.
Establishes dimension-independent polynomial influence bounds addressing the Aaronson–Ambainis conjecture, supported by general determinant, fractional-certificate, level-set and coordinate-averaging results.
Tokens: 16,605,183 in / 35,223 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $66.9491 (Standard API equivalent; uncached input)
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.
|
Addressed the novelty finding from the review of I inspected All Lean source files are byte-identical to the fully validated and profiled |
|
/review |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Thorough review update at d8fa135cf2783fa4e950089ed30fad337da436be: approve, with no unresolved author-actionable findings.
I inspected the existing StandardLP.strongDuality and attainment/feasibility definitions and confirmed the configured review's supporting-LP overlap. The card now advertises only the four influence endpoints and explicitly credits the pooled generic LP theorem. The internal supporting proof retains its original generality. All 84 Lean modules are byte-identical to the previously reviewed source; the complete new diff since that checkpoint is this card correction.
Current-head Lean CI passes build, declaration lint, style, and quality/trust checks. Every protected context completed successfully or was skipped by its applicable path filter. Current-head profiling passes all 84 files (877,314 heartbeat units; 72.76s changed-module build), and Greptile reports no blocking code issue or new inline finding.
The configured GPT review of the corrected card remains required before native-queue admission. The previous review and its finding are preserved in the PR discussion and acquisition evidence; this follow-up does not substitute for that configured verdict.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent source continuation at exact head d8fa135 (permanent-reviewer Source152).
Source accepted. I verified the native commit and complete tree delta: only LeanPool/projects/aaronson-ambainis.yaml changed from 29a1ba2. All 84 Lean files, the facade and import graph are byte-identical, so the complete mathematical, provenance and quality review in Source151 applies to those unchanged bodies.
The novelty concern in configured review 2400 is substantiated: the supporting packing-cover implication follows from the existing StandardLP.strongDuality and optimum_neq_none by finite incidence-matrix specialization and attainment. This includes the empty-index and empty-set cases without adding assumptions. The corrected card now credits that result and reserves main_results for the four influence endpoints. Retaining the upstream self-contained geometric proof as supporting code is acceptable; the card makes no claim that generic finite LP duality is new.
The unchanged chain establishes the unconditional (epsilon/d)^7 influence result and the two explicit normalization variants; the stronger fractional block-sensitivity constant remains explicitly conditional. The fixed upstream Apache-2.0 license, AI provenance, paper correspondence and bounded current-library comparisons remain as reviewed. No mathematical statement or proof was weakened.
This is source acceptance at this head. CI from 29a1 and its configured review do not qualify d8fa. The newly requested configured review and all applicable checks still need to pass before protected-queue admission, consistent with the author's current readiness condition.
Imports the completed proof of the Aaronson–Ambainis influence conjecture and its reusable finite-cube, determinant, fractional-certificate, averaging and packing/cover infrastructure.
For a real polynomial bounded in
[0,1]on the Boolean cube, degree at mostdand positive variance at leastε, the unconditional endpoint proves a coordinate has squared-difference influence at least(ε/d)^7. Two further unconditional endpoints give the explicitε^(5/2)/d^6bounds in the zero-one and sign-cube normalizations. The sharper constant is explicitly conditional onFbsDegreeBound; quantum simulation consequences are outside the imported scope.2026-11-01T10:15:13Z–2026-11-08T10:15:13Z.2a6ceaef872ae993708950f951989134084b851a, Apache-2.0, provenance AI. David Turturean's attribution, relevant NOTICE text and modification notices are retained.The internal packing-cover lemma
Dual.exists_coverspecializes generic finite LP duality already pooled asStandardLP.strongDualityinLeanPool.Duality.LinearProgrammingB. The card credits that prior result and advertises the influence endpoints. The supporting upstream proof via Mathlib geometric separation remains self-contained within this import.Ported to Lean 4.35.0 and Mathlib
56a005855ea17e0b0958f73ec801ae140b0a1679: module/public/expose declarations, scoped imports and namespaces, coefficient-field API, deprecated theorem names, redundant tactics and unused instance hypotheses. Removed diagnostics and fixed comment/whitespace issues. Theorem strength and reusable generality are preserved. The fixedLeanPool.lean, CI, rules, linters and gates are unchanged.Measured optimization: both runs freshly compiled all 84 project modules against cached exact dependencies, using
/usr/bin/time -v env LEAN_NUM_THREADS=4 lake build LeanPool.AaronsonAmbainis.Importson the same shared VM. Baseline 124.24s wall / 256.60s user / 60.65s system / 3,064,708 KB peak RSS; final optimized 81.65s / 130.68s / 37.26s / 1,525,272 KB, a 34.3% wall-time reduction and 49.1% user-CPU reduction. Summed overlapping per-module wall times fell from 399.7s to 283.6s. Replaced five broad Mathlib imports using compiled declaration dependencies and explicit tactic imports, and consolidated eight duplicate degree-calculus proofs through existing lemmas. Addressed Greptile’s repeated-proof finding by sharing cube identities, character multiplication, and lowest-monomial existence while preserving namespace aliases. An earlier optimized clean run measured 55.94s; shared-VM utilization varied, so the final-head measurement is reported above. Profiled slow arithmetic, third-moment and bridge declarations; no further material safe improvement was evident. No heartbeat overrides or trust escape hatches were added.Local validation: complete warning-as-error project build; generated indexes; style checks; static repository quality; compiled declaration linters (738 declarations) and complete 84-module axiom/option-backdoor audits. No Python sources changed. CI remains the authority for combined-tree required checks. Configured Greptile and GPT reviews plus a separate thorough review are required before protected native-queue entry.