Repository navigation
Reduce IwaniecLinearSieve arithmetic elaboration cost - #772
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] The proof-only refactor appears safe to merge; no blocking issue was found. SummaryThis refactor narrows arithmetic proof searches across 36 existing Lean modules while preserving the surrounding arguments.
Reviews (1) · Last reviewed commit: "perf(IwaniecLinearSieve): narrow arithme..." · Reviewed by Greptile |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 1,057 tracked declarations across 36 modified files kept their type; only proofs / definition bodies changed. Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 6,923,980 → 5,766,888 (-1,157,092, -16.7%). Commands: 1,931 → 1,931. Per-file wall sum: 615.5 s → 560.3 s (-9.0%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 36 compared — 25 cheaper, 1 costlier, 10 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%). Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from disjoint root command traces with
Advisory only — never blocks merge. Full log uploaded as the |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "Technical source review at exact 94c8f24: all 354 changed written proof envelopes are covered. Independent normalization isolates 341 tactic-input changes; the remaining 13 arguments were reviewed separately, including the positive factored cubic bound, reuse of the existing large-xi/max witnesses, and BigO multiplication/norm/eventual-congruence route for the logarithmic tail integral. Required signs, thresholds, endpoint hypotheses and theorem conclusions are retained. Written headers and nonproof values are preserved, with no added or removed declarations. The sole private import removal leaves public import vectors unchanged; actual elaboration remains a hosted-CI requirement. The author's generated-declaration audit and measured speedup were not independently reproduced. Current-head protected CI and native integration remain required.",
"assessment": {
"scope": "existing IwaniecLinearSieve proof elaboration and one private import removal",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Explicit tactic inputs and standard analytic composition expose the needed arguments without weakening statements or replacing reusable interfaces."
},
"verdict": "approve",
"findings": []
}
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | arithmetic tactic and analytic proof refactor |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
Explicit arithmetic dependencies and standard lemma composition make these proofs easier to debug and less sensitive to unrelated context without sacrificing reusable structure.
Tokens: 4,091,453 in / 8,032 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $16.4863 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
IwaniecLinearSieve spends substantial elaboration time normalizing unrelated local inequalities in arithmetic proofs. This change restricts those searches and reuses existing analytic bounds. On the Azure VM, the median clean project build fell from 386.215s to 328.165s (15.03% faster) across two quiet measurements per revision.
linarithandnlinarithexplicit hypothesis lists while preserving the surrounding proof structure and existing explicit lemma inputs.TheoremFive.crude_exponent_lewith a factored product comparison; restrict its remaining exponential estimates to their relevant inequalities.TheoremFive.exists_card_smallinstead of reconstructing those bounds through logarithmic comparisons.IsBigOmultiplication, norm and congruence results inintegrable_log_over_pow; use explicit monotonicity and nonnegativity arguments in the analytic support proofs.Mathlib.Algebra.Order.Star.Realimport inTheoremFiveCount, as reported bylake shake.Invariant audit: Before editing, a standalone Lean environment inspector imported all 48 project modules at private visibility and exported every declaration's full type expression DAG, universe parameters, kind, safety, mutual-declaration information, and non-theorem value/reducibility information. The final clean-build export matches all 2,575 module/name records (2,573 distinct names) exactly in those fields, including compiler-generated private helpers. All 243 definition values are identical. There are no added or removed declarations; only 312 theorem proof bodies differ. Types are compared structurally, including binder names and annotations, rather than by pretty-printed text.
Measured/audited base:
49bdad2b2b82b4b41d75a8e251ac10b2aa08fb45Head:
94c8f24e3f70c5536e81d509ce8b6a8c45e7006eMain advanced to
5bf7f7139f861a1e548dff28e2e747fb66d472f4during the cycle. The selected project, its MooreBound dependency, pinned toolchain/dependency manifest, and relevant contribution/review/quality rules are unchanged from the measured base. The measured head is preserved without rebasing.Measurements: Both revisions use the repository-pinned Lean/Mathlib 4.35.0, unchanged Lake options and compiler linters,
LEAN_NUM_THREADS=1, and CPU affinity 14 on the same AMD EPYC 9V45 Azure VM. Before each run, only this project's artifacts under.lake/build/lib/lean/LeanPool/IwaniecLinearSieve*and.lake/build/ir/LeanPool/IwaniecLinearSieve*were deleted. Mathlib and unchanged dependency artifacts were retained and warmed. All 48 project modules were rebuilt using:Median RSS: 2,056,320 → 2,052,340 KiB, effectively unchanged. Mean aggregate user+system CPU time: 367.460 → 317.425s (13.62% lower). The reported wall-time improvement is the ratio of the two per-revision medians. Shared VM load caused visible timing variation; these measurements do not establish the same speedup on parallel CI runners. An exploratory baseline that overlapped a diagnostic compiler on CPU 14's SMT sibling was excluded from this table.
Validation on the final source:
lake build LeanPool.IwaniecLinearSieve.Imports, including the normal warning-as-error and proof-size plugin checks; all timed clean builds passed.lake env lean --run scripts/ci/lint-project.leanover all 48 owned modules: slow Mathlib declaration linters passed (2,572 owner-filtered declarations).lake exe lint-style LeanPool.IwaniecLinearSieve.Importsandgit diff --check: passed.lake shake --force --keep-public LeanPool.IwaniecLinearSieve.Imports: no remaining selected-project suggestions. It still reports suggestions in unchanged MooreBound dependencies, outside this PR's scope.The PR changes only this existing project's Lean sources. Public imports, project metadata, generated indexes, toolchain pins, repository checks and waivers are unchanged. Full protected CI and the independent refactor review remain applicable. Auto-merge is disabled.