Repository navigation
Import Iwaniec's linear sieve and Jacobsthal bound - #700
Merged
Merged
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low impact] The latest proof refactors preserve the existing theorem statements; no blocking code issue was established. SummaryImports Iwaniec’s Jacobsthal bound with its sieve and prime-number-theorem dependencies. The latest changes share the zeta estimates and shorten two existing proofs.
Reviews (5) · Last reviewed commit: "refactor(IwaniecLinearSieve): share zeta..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Collaborator
Author
{
"verdict": "approve",
"reviewed_commit": "2d7d6005157a0660dc7c0a043a074ad11a3ba581",
"reviewer_role": "Additional acquisition-agent review: a separate author-side pass, alongside the configured independent GPT reviews.",
"coverage": "Checked the complete 49-file diff and exact upstream snapshot, each file's imports/declaration inventory, all advertised endpoints and their dependency closure, and bounded implementation slices across the sieve, delay equations, prime estimates, contour arguments and PNT. The temporary unconsumed residue section identified by Greptile was removed and revalidated.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The public endpoint proves the advertised absolute covering-run bound without unproved analytic inputs.",
"proves_the_claim": "proves_it",
"claim_note": "iwaniecBound quantifies one C before every finite set S of primes with 2 ≤ S.card, every integer starting point x and every natural run length m; divisibility of each x+k implies m ≤ C (S.card * log S.card)^2. shiftedSieve gives the lower sieve count for arbitrary prime sets of the requisite cardinality, and linearSieveEstimate proves its asymptotic main-term/support estimates.",
"assumed_inputs": "",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate Jacobsthal endpoint was found in the pinned Mathlib, Tau Ceti, pool sources/cards, PRs, issues or history.",
"already_formalized": "",
"novelty_note": "Mathlib's Selberg sieve and the existing pool PNT foundations do not provide this Rosser-Iwaniec lower sieve at the sifting limit; five existing PNT modules are reused rather than copied.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "A serious research formalization with useful analytic and combinatorial infrastructure.",
"fit": "good_fit",
"level": "research",
"branch": "analytic number theory",
"mode": "mixed",
"significance_one_sentence": "Preserves Iwaniec's classical quadratic-logarithmic Jacobsthal bound together with Rosser weights, delay-equation majorants, prime-sum estimates and its proved strong-PNT input.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The run-length formulation matches the 1978 Corollary, and the partial-import scope and PNT attribution are explicit.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "Competent port after removing blueprint machinery, unrelated imports and unused temporary API, factoring repeated estimates and splitting expensive analytic assembly; no waivers or source options remain.",
"code_quality": 3,
"findings": []
},
"evidence": {
"upstream": "https://github.com/jasondavies/iwaniec-linear-sieve/tree/c8d01549d2ae640b36ec198c1f0f6495f1b036cf",
"announcement": "2026-10-20 11:58:42 UTC, https://leanprover.zulipchat.com/#narrow/channel/583339/near/633293145",
"source_paper": "Iwaniec, On the problem of Jacobsthal, Demonstratio Mathematica 11 (1978), Corollary p. 226; DOI 10.1515/dema-1978-0121, checked against the original paper's publisher-provided ResearchGate reproduction.",
"license_provenance": "Apache-2.0 code; mixed provenance records the AI-authored sieve and substantial separately credited earlier PNT contributions.",
"local_validation": "Warning-free clean build and public Imports wrapper; Mathlib declaration lint for 48 modules/2,607 declarations; style; full repository static quality; generated-index verification; main-card declarations; axiom and option audit of all 2,610 compiled declarations including private constants, with only the allowed axioms and no forbidden option references.",
"compile_measurements": "Sequential archived baseline → final: 348.238 → 178.052 wall seconds; 563.720 → 407.116 aggregate child CPU seconds. LEAN_NUM_THREADS=4; clean project outputs; identical pinned package cache. Initial baseline 205.318 seconds and intermediate 240.542 seconds show host variability.",
"profiles": "The baseline synchronous GenStrengthPNT profile exceeded 200,000 heartbeats; the final MediumPNT file profiles successfully under default limits. I1Bound: 61,046 → 32,097 heartbeats; SmoothedChebyshevClose_aux: 78,612 → 61,577. Final GenStrengthPNT 54,737 plus extracted contour assembly 90,328.",
"protected_ci": "Still running on this exact head. Queue entry requires protected CI and the configured independent GPT verdict to pass."
},
"remaining_findings": []
} |
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: 7,161,295 maxHeartbeats units across 48 valid files (23,295 added LOC). Sum of Count-heartbeats wall-clock total: 893.92 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.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.ZetaBounds |
35.00 s |
LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.MediumPNT |
19.00 s |
LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.StrongPNT |
17.00 s |
LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.MellinCalculus |
14.00 s |
LeanPool.IwaniecLinearSieve.SieveMajorants.Lemmas |
14.00 s |
LeanPool.IwaniecLinearSieve.Vendor.PrimeNumberTheoremAnd.ResidueCalcOnRectangles |
12.00 s |
LeanPool.IwaniecLinearSieve.LinearSieve.Depth |
11.00 s |
LeanPool.IwaniecLinearSieve.LinearSieve.TheoremFiveAux |
9.60 s |
LeanPool.IwaniecLinearSieve.SieveMajorants.Properties |
9.50 s |
LeanPool.IwaniecLinearSieve.LinearSieve.Estimate |
9.10 s |
LeanPool.IwaniecLinearSieve.LinearSieve.LemmaEleven |
8.90 s |
LeanPool.IwaniecLinearSieve.LinearSieve.Corollaries |
8.80 s |
Per-file `lean --profile` output
LeanPool/IwaniecLinearSieve.lean
import took 2.26s
cumulative profiling times:
elaboration 0.186ms
import 2.26s
initialization 25.7ms
interpretation 159ms
linting 0.413ms
module linting 0.00149ms
overlappingInstancesLinter 0.368ms
parsing 0.0287ms
tacticAnalysis 2.23ms
real 3.06
user 1.05
sys 0.99
LeanPool/IwaniecLinearSieve/Basic.lean
import took 1.02s
cumulative profiling times:
attribute application 0.0349ms
congr simp thm 0.536ms
elaboration 16.9ms
fix level params 0.0793ms
import 1.02s
initialization 34.4ms
instantiate metavars 0.0569ms
interpretation 196ms
let-to-have transformation 0.0327ms
linting 3.14ms
module linting 0.0015ms
overlappingInstancesLinter 1.81ms
parsing 1.37ms
process pre-definitions 0.871ms
share common exprs 0.356ms
simp 6.42ms
tactic execution 7.9ms
tacticAnalysis 7.84ms
type checking 5.42ms
typeclass inference 38.1ms
real 1.87
user 1.12
sys 0.86
LeanPool/IwaniecLinearSieve/Definitions.lean
import took 1.04s
cumulative profiling times:
attribute application 0.0927ms
compilation (IR) 0.131ms
compilation (LCNF base) 1.92ms
compilation (LCNF impure) 0.726ms
compilation (LCNF mono) 0.993ms
elaboration 25ms
fix level params 0.087ms
import 1.04s
initialization 25.6ms
instantiate metavars 0.112ms
interpretation 215ms
let-to-have transformation 0.0858ms
linting 6.57ms
module linting 0.00132ms
overlappingInstancesLinter 2.71ms
parsing 5.04ms
process pre-definitions 6.3ms
share common exprs 0.47ms
tacticAnalysis 12.5ms
type checking 7.81ms
typeclass inference 33ms
real 1.91
user 1.14
sys 0.89
LeanPool/IwaniecLinearSieve/Imports.lean
import took 1.08s
cumulative profiling times:
elaboration 0.0876ms
import 1.08s
initialization 25.9ms
interpretation 155ms
linting 0.205ms
module linting 0.00142ms
overlappingInstancesLinter 0.0931ms
parsing 0.00196ms
tacticAnalysis 0.39ms
real 1.88
user 1.04
sys 0.88
LeanPool/IwaniecLinearSieve/Jacobsthal.lean
import took 1.08s
cumulative profiling times:
attribute application 0.0094ms
elaboration 5.79ms
fix level params 0.0119ms
import 1.08s
initialization 25.9ms
instantiate metavars 0.0182ms
interpretation 177ms
let-to-have transformation 0.0232ms
linting 1.57ms
module linting 0.0014ms
overlappingInstancesLinter 0.788ms
parsing 0.961ms
process pre-definitions 0.132ms
share common exprs 0.0714ms
tacticAnalysis 5.3ms
type checking 0.341ms
typeclass inference 4.91ms
real 1.90
user 1.07
sys 0.88
LeanPool/IwaniecLinearSieve/Jacobsthal/Reduction.lean
import took 1.08s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 164ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 321ms
cumulative profiling times:
attribute application 0.0435ms
congr simp thm 8.32ms
elaboration 29.3ms
fix level params 1.03ms
import 1.08s
initialization 25.9ms
instantiate metavars 7.59ms
interpretation 1.32s
let-to-have transformation 0.0768ms
linting 16.4ms
module linting 0.00137ms
norm_num 119ms
overlappingInstancesLinter 3.13ms
parsing 10.8ms
process pre-definitions 22.7ms
ring 71ms
share common exprs 18.1ms
simp 212ms
tactic execution 241ms
tacticAnalysis 41.5ms
type checking 124ms
typeclass inference 537ms
real 3.52
user 3.66
sys 0.88
LeanPool/IwaniecLinearSieve/Jacobsthal/ShiftedSieve.lean
import took 1.06s
cumulative profiling times:
attribute application 0.169ms
blocked (unaccounted) 0.0513ms
congr simp thm 15.4ms
elaboration 79.9ms
fix level params 1.67ms
import 1.06s
initialization 24.9ms
instantiate metavars 6.49ms
interpretation 667ms
let-to-have transformation 0.3ms
linting 65.8ms
module linting 0.0015ms
norm_num 114ms
overlappingInstancesLinter 7.95ms
parsing 26.5ms
process pre-definitions 20.8ms
ring 46.8ms
share common exprs 18.4ms
simp 431ms
tactic execution 536ms
tacticAnalysis 84.6ms
type checking 141ms
typeclass inference 711ms
real 2.77
user 3.80
sys 0.91
LeanPool/IwaniecLinearSieve/LinearSieve/Calculus.lean
import took 1.04s
cumulative profiling times:
attribute application 2.35ms
compilation (IR) 0.268ms
compilation (LCNF base) 4.52ms
compilation (LCNF impure) 1.21ms
compilation (LCNF mono) 1.71ms
congr simp thm 1.78ms
elaboration 113ms
fix level params 1.32ms
import 1.04s
initialization 24.9ms
instantiate metavars 1.76ms
interpretation 555ms
let-to-have transformation 0.311ms
linting 21.9ms
module linting 0.00159ms
norm_num 28.2ms
overlappingInstancesLinter 5.63ms
parsing 13.9ms
process pre-definitions 13.5ms
ring 56.8ms
share common exprs 14.5ms
simp 64.4ms
tactic execution 170ms
tacticAnalysis 34.2ms
type checking 98.8ms
typeclass inference 366ms
real 2.42
user 2.39
sys 0.89
LeanPool/IwaniecLinearSieve/LinearSieve/Corollaries.lean
import took 1.09s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 102ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 220ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 127ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 174ms
interpretation of Mathlib.Meta.Positivity.evalMul._lam_3._boxed took 119ms
tactic execution of Mathlib.Tactic.nlinarith took 858ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.31s
cumulative profiling times:
attribute application 0.232ms
congr simp thm 14.6ms
elaboration 235ms
fix level params 5.86ms
import 1.09s
initialization 25.2ms
instantiate metavars 26.6ms
interpretation 6.75s
let-to-have transformation 0.635ms
linting 93.6ms
module linting 0.00146ms
norm_num 1.64s
overlappingInstancesLinter 10.5ms
parsing 53.2ms
process pre-definitions 86ms
ring 398ms
share common exprs 108ms
simp 232ms
tactic execution 2.28s
tacticAnalysis 161ms
type checking 366ms
typeclass inference 3.32s
real 7.18
user 16.57
sys 0.97
LeanPool/IwaniecLinearSieve/LinearSieve/Crude.lean
import took 1.1s
cumulative profiling times:
attribute application 0.179ms
congr simp thm 7.47ms
elaboration 75.9ms
fix level params 2.01ms
import 1.1s
initialization 25.2ms
instantiate metavars 3.7ms
interpretation 1.03s
let-to-have transformation 0.289ms
linting 42.6ms
module linting 0.00142ms
norm_num 42.3ms
overlappingInstancesLinter 6.11ms
parsing 26.4ms
process pre-definitions 25.3ms
ring 61.2ms
share common exprs 18.2ms
simp 273ms
tactic execution 762ms
tacticAnalysis 82.9ms
type checking 147ms
typeclass inference 1.15s
real 3.24
user 4.58
sys 0.94
LeanPool/IwaniecLinearSieve/LinearSieve/Defs.lean
import took 1.04s
cumulative profiling times:
attribute application 0.0288ms
compilation (IR) 0.127ms
compilation (LCNF base) 3.59ms
compilation (LCNF impure) 0.559ms
compilation (LCNF mono) 0.863ms
elaboration 9.22ms
fix level params 0.0337ms
import 1.04s
initialization 29.1ms
instantiate metavars 0.0498ms
interpretation 181ms
let-to-have transformation 0.03ms
linting 2.47ms
module linting 0.00169ms
overlappingInstancesLinter 1.47ms
parsing 1.79ms
process pre-definitions 1.75ms
share common exprs 0.166ms
tacticAnalysis 5.33ms
type checking 1.23ms
typeclass inference 14.9ms
real 1.89
user 1.07
sys 0.88
LeanPool/IwaniecLinearSieve/LinearSieve/Depth.lean
import took 1.06s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 150ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 271ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 564ms
cumulative profiling times:
attribute application 0.161ms
blocked (unaccounted) 1.45ms
congr simp thm 6.97ms
elaboration 60.2ms
fix level params 1.9ms
import 1.06s
initialization 25.1ms
instantiate metavars 5.04ms
interpretation 1.86s
let-to-have transformation 0.208ms
linting 33.3ms
module linting 0.00154ms
norm_num 129ms
overlappingInstancesLinter 5.57ms
parsing 17.9ms
process pre-definitions 23.2ms
ring 89.1ms
share common exprs 24.3ms
simp 118ms
tactic execution 414ms
tacticAnalysis 65.7ms
type checking 162ms
typeclass inference 706ms
real 4.20
user 4.51
sys 0.89
LeanPool/IwaniecLinearSieve/LinearSieve/Estimate.lean
import took 1.09s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.86s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 2.09s
interpretation of Mathlib.Meta.Positivity.evalDiv._lam_0._boxed took 150ms
cumulative profiling times:
attribute application 0.0772ms
compilation (IR) 0.0586ms
compilation (LCNF base) 0.369ms
compilation (LCNF impure) 0.247ms
compilation (LCNF mono) 0.369ms
congr simp thm 6.24ms
dsimp 2.07ms
elaboration 45.4ms
fix level params 2.34ms
import 1.09s
initialization 31.7ms
instantiate metavars 12.2ms
interpretation 5.9s
let-to-have transformation 0.118ms
linting 32.4ms
module linting 0.00152ms
norm_num 209ms
overlappingInstancesLinter 4.06ms
parsing 14.2ms
process pre-definitions 56.1ms
ring 147ms
share common exprs 43ms
simp 524ms
tactic execution 616ms
tacticAnalysis 60.1ms
type checking 133ms
typeclass inference 945ms
real 9.55
user 9.60
sys 0.93
LeanPool/IwaniecLinearSieve/LinearSieve/LemmaEleven.lean
import took 1.05s
cumulative profiling times:
attribute application 0.269ms
blocked (unaccounted) 83.4ms
congr simp thm 3.84ms
dsimp 4.52ms
elaboration 287ms
fix level params 5.96ms
import 1.05s
initialization 25.3ms
instantiate metavars 20.2ms
interpretation 2.19s
let-to-have transformation 0.722ms
linting 116ms
module linting 0.00171ms
norm_num 730ms
overlappingInstancesLinter 8.95ms
parsing 40.6ms
process pre-definitions 83.5ms
ring 387ms
share common exprs 107ms
simp 37ms
tactic execution 1s
tacticAnalysis 118ms
type checking 379ms
typeclass inference 2.81s
real 4.62
user 9.14
sys 0.93
LeanPool/IwaniecLinearSieve/LinearSieve/LemmaSeven.lean
import took 1.06s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 143ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 121ms
cumulative profiling times:
attribute application 0.117ms
blocked (unaccounted) 2.28ms
congr simp thm 1.51ms
elaboration 50.3ms
fix level params 2.61ms
import 1.06s
initialization 25ms
instantiate metavars 6.94ms
interpretation 1.49s
let-to-have transformation 0.187ms
linting 34.5ms
module linting 0.00139ms
norm_num 271ms
overlappingInstancesLinter 3.17ms
parsing 9.71ms
process pre-definitions 33ms
ring 183ms
share common exprs 55.6ms
simp 12.2ms
tactic execution 199ms
tacticAnalysis 27.3ms
type checking 157ms
typeclass inference 715ms
real 2.89
user 4.06
sys 0.91
LeanPool/IwaniecLinearSieve/LinearSieve/TheoremFive.lean
import took 1.08s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 167ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 165ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 150ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 395ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 460ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 247ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 370ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 396ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 460ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 111ms
cumulative profiling times:
attribute application 0.154ms
congr simp thm 10.7ms
elaboration 127ms
fix level params 3.87ms
import 1.08s
initialization 25.4ms
instantiate metavars 14.1ms
interpretation 5.44s
let-to-have transformation 0.402ms
linting 89.6ms
module linting 0.00138ms
norm_num 563ms
overlappingInstancesLinter 8.75ms
parsing 34.3ms
process pre-definitions 59ms
ring 251ms
share common exprs 58.4ms
simp 339ms
tactic execution 867ms
tacticAnalysis 129ms
type checking 217ms
typeclass inference 2.58s
real 5.67
user 11.59
sys 0.91
LeanPool/IwaniecLinearSieve/LinearSieve/TheoremFiveAux.lean
import took 1.09s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 150ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 339ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 325ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 552ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 611ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 572ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 699ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 656ms
cumulative profiling times:
attribute application 0.807ms
congr simp thm 1.95ms
dsimp 16.8ms
elaboration 68ms
fix level params 2.41ms
import 1.09s
initialization 25.3ms
instantiate metavars 7.7ms
interpretation 4.93s
let-to-have transformation 0.208ms
linting 43.1ms
module linting 0.0015ms
norm_num 392ms
overlappingInstancesLinter 4.16ms
parsing 12.4ms
process pre-definitions 33.9ms
ring 163ms
share common exprs 46.3ms
simp 19ms
tactic execution 294ms
tacticAnalysis 35.4ms
type checking 126ms
typeclass inference 1.1s
real 7.20
user 8.12
sys 0.92
LeanPool/IwaniecLinearSieve/LinearSieve/TheoremFiveCount.lean
import took 1.12s
cumulative profiling times:
attribute application 0.144ms
congr simp thm 13.2ms
dsimp 1.74ms
elaboration 108ms
fix level params 4.34ms
import 1.12s
initialization 25.2ms
instantiate metavars 32.2ms
interpretation 2.63s
let-to-have transformation 0.292ms
linting 71.4ms
module linting 0.00171ms
norm_num 648ms
overlappingInstancesLinter 8.09ms
parsing 33ms
process pre-definitions 77.1ms
ring 343ms
share common exprs 94.3ms
simp 348ms
tactic execution 1.32s
tacticAnalysis 122ms
type checking 280ms
typeclass inference 1.12s
real 4.66
user 8.09
sys 0.96
LeanPool/IwaniecLinearSieve/LinearSieve/TheoremFour.lean
import took 1.14s
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 121ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 340ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 306ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 350ms
tactic execution of Mathlib.Tactic.nlinarith took 203ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 125ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 235ms
tactic execution of Mathlib.Tactic.nlinarith took 584ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 379ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 787ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 455ms
cumulative profiling times:
attribute application 0.205ms
congr simp thm 17.1ms
elaboration 213ms
fix level params 4.93ms
import 1.14s
initialization 25.3ms
instantiate metavars 33.2ms
interpretation 6.23s
let-to-have transformation 0.55ms
linting 115ms
module linting 0.00151ms
norm_num 1.05s
overlappingInstancesLinter 12.3ms
parsing 47.5ms
process pre-definitions 92.7ms
ring 283ms
share common exprs 74.9ms
simp 733ms
tactic execution 2.12s
tacticAnalysis 175ms
type checking 294ms
typeclass inference 3.29s
real 6.00
user 15.65
sys 0.96
LeanPool/IwaniecLinearSieve/LinearSieve/TheoremFourAsymp.lean
import took 1.1s
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 104ms
cumulative profiling times:
attribute application 0.188ms
blocked (unaccounted) 647ms
congr simp thm 3.6ms
dsimp 37.1ms
elaboration 185ms
fix level params 5.38ms
import 1.1s
initialization 25ms
instantiate metavars 20.3ms
interpretation 2.31s
let-to-have transformation 0.462ms
linting 98.6ms
module linting 0.00152ms
norm_num 857ms
overlappingInstancesLinter 8.27ms
parsing 30.4ms
process pre-definitions 88.5ms
ring 349ms
share common exprs 113ms
simp 37ms
tactic execution 1.19s
tacticAnalysis 104ms
type checking 286ms
typeclass inference 1.37s
real 4.43
user 7.88
sys 0.94
LeanPool/IwaniecLinearSieve/LinearSieve/TheoremFourAux.lean
import took 1.11s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 167ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 253ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 358ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 315ms
cumulative profiling times:
attribute application 0.178ms
congr simp thm 6.27ms
elaboration 70.2ms
fix level params 2.2ms
import 1.11s
initialization 24.8ms
instantiate metavars 5.89ms
interpretation 2.25s
let-to-have transformation 0.255ms
linting 60.3ms
module linting 0.00159ms
norm_num 474ms
overlappingInstancesLinter 6.3ms
parsing 18.1ms
process pre-definitions 30.4ms
ring 155ms
share common exprs 34.7ms
simp 117ms
tactic execution 434ms
tacticAnalysis 53.3ms
type checking 143ms
typeclass inference 833ms
real 4.58
user 5.54
sys 0.95
LeanPool/IwaniecLinearSieve/PrimeSums.lean
import took 1.12s
cumulative profiling times:
elaboration 0.307ms
import 1.12s
initialization 25.8ms
interpretation 168ms
linting 0.652ms
module linting 0.00137ms
overlappingInstancesLinter 0.454ms
parsing 0.24ms
tacticAnalysis 1.12ms
real 1.95
user 1.10
sys 0.89
LeanPool/IwaniecLinearSieve/PrimeSums/Error.lean
import took 1.15s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 280ms
cumulative profiling times:
attribute application 0.158ms
blocked (unaccounted) 0.46ms
congr simp thm 1.47ms
elaboration 50.3ms
fix level params 1.79ms
import 1.15s
initialization 25.6ms
instantiate metavars 2.91ms
interpretation 1.18s
let-to-have transformation 0.2ms
linting 28.4ms
module linting 0.00184ms
norm_num 173ms
overlappingInstancesLinter 5.08ms
parsing 11.7ms
process pre-definitions 20.6ms
ring 107ms
share common exprs 27.9ms
simp 10.1ms
tactic execution 360ms
tacticAnalysis 39.9ms
type checking 107ms
typeclass inference 657ms
real 2.89
user 3.64
sys 0.96
LeanPool/IwaniecLinearSieve/PrimeSums/Lemma13.lean
import took 1.13s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 386ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 265ms
cumulative profiling times:
attribute application 0.319ms
blocked (unaccounted) 0.279ms
congr simp thm 8.77ms
elaboration 133ms
fix level params 3.37ms
import 1.13s
initialization 25.4ms
instantiate metavars 11.6ms
interpretation 2.31s
let-to-have transformation 0.465ms
linting 57.3ms
module linting 0.00147ms
norm_num 232ms
overlappingInstancesLinter 10.3ms
parsing 34.6ms
process pre-definitions 49.9ms
ring 221ms
share common exprs 52.7ms
simp 217ms
tactic execution 742ms
tacticAnalysis 95.7ms
type checking 326ms
typeclass inference 1.01s
real 3.69
user 6.36
sys 0.95
LeanPool/IwaniecLinearSieve/PrimeSums/Mertens.lean
import took 1.13s
interpretation of Mathlib.Meta.FunProp.funPropTac._boxed took 141ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 209ms
tactic execution of Mathlib.Tactic.nlinarith took 129ms
cumulative profiling times:
attribute application 0.142ms
blocked (unaccounted) 106ms
congr simp thm 4.5ms
dsimp 1.54ms
elaboration 72.3ms
fix level params 2.68ms
import 1.13s
initialization 32.5ms
instantiate metavars 6.39ms
interpretation 1.49s
let-to-have transformation 0.268ms
linting 45ms
module linting 0.00154ms
norm_num 202ms
overlappingInstancesLinter 6.1ms
parsing 19.1ms
process pre-definitions 28.4ms
ring 159ms
share common exprs 48.2ms
simp 64.7ms
tactic execution 778ms
tacticAnalysis 54.9ms
type checking 203ms
typeclass inference 963ms
real 3.29
user 5.03
sys 0.92
LeanPool/IwaniecLinearSieve/PrimeSums/NthPrime.lean
import took 1.07s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 123ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 145ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 163ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 174ms
cumulative profiling times:
attribute application 0.027ms
congr simp thm 1.76ms
elaboration 13.9ms
fix level params 0.916ms
import 1.07s
initialization 25.4ms
instantiate metavars 3.4ms
interpretation 1.1s
let-to-have transformation 0.0366ms
linting 6.02ms
module linting 0.00156ms
norm_num 108ms
overlappingInstancesLinter 1.58ms
parsing 3.51ms
process pre-definitions 8.62ms
ring 56.4ms
share common exprs 25.1ms
simp 19.7ms
tactic execution 112ms
tacticAnalysis 14ms
type checking 54.3ms
typeclass inference 355ms
real 3.42
user 2.78
sys 0.85
LeanPool/IwaniecLinearSieve/PrimeSums/Product.lean
import took 1.13s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 457ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 453ms
cumulative profiling times:
attribute application 0.153ms
blocked (unaccounted) 0.717ms
congr simp thm 4.12ms
elaboration 56.5ms
fix level params 2.07ms
import 1.13s
initialization 25.6ms
instantiate metavars 9.68ms
interpretation 1.95s
let-to-have transformation 0.192ms
linting 38.1ms
module linting 0.00143ms
norm_num 140ms
overlappingInstancesLinter 5.28ms
parsing 17.2ms
process pre-definitions 28.4ms
ring 150ms
share common exprs 32.3ms
simp 47.5ms
tactic execution 436ms
tacticAnalysis 55.1ms
type checking 129ms
typeclass inference 719ms
real 3.74
user 4.66
sys 0.98
LeanPool/IwaniecLinearSieve/PrimeSums/SummationByParts.lean
import took 1.06s
cumulative profiling times:
attribute application 0.0225ms
congr simp thm 1.76ms
elaboration 21ms
fix level params 0.643ms
import 1.06s
initialization 25.6ms
instantiate metavars 2.53ms
interpretation 443ms
let-to-have transformation 0.0569ms
linting 21.4ms
module linting 0.00157ms
norm_num 4.1ms
overlappingInstancesLinter 1.88ms
parsing 8.12ms
process pre-definitions 9.88ms
ring 36.6ms
share common exprs 10.9ms
simp 24.8ms
tactic execution 231ms
tacticAnalysis 25.7ms
type checking 45.3ms
typeclass inference 212ms
real 2.47
user 1.98
sys 0.89
LeanPool/IwaniecLinearSieve/Rosser.lean
import took 1.06s
simp took 180ms
cumulative profiling times:
attribute application 3ms
blocked (unaccounted) 0.815ms
congr simp thm 8.63ms
elaboration 137ms
fix level params 1.67ms
import 1.06s
initialization 26.1ms
instantiate metavars 3.58ms
interpretation 592ms
let-to-have transformation 0.583ms
linting 53.7ms
module linting 0.0014ms
norm_num 9.23ms
overlappingInstancesLinter 14.4ms
parsing 28.3ms
process pre-definitions 24.3ms
ring 12.3ms
share common exprs 11.2ms
simp 495ms
tactic execution 382ms
tacticAnalysis 91ms
type checking 83.1ms
typeclass inference 542ms
real 2.50
user 3.28
sys 0.94
LeanPool/IwaniecLinearSieve/SieveFunctions.lean
import took 1.07s
cumulative profiling times:
elaboration 0.34ms
import 1.07s
initialization 25.8ms
interpretation 166ms
linting 0.638ms
module linting 0.00164ms
overlappingInstancesLinter 0.397ms
parsing 0.208ms
tacticAnalysis 1.24ms
real 1.88
user 1.03
sys 0.88
LeanPool/IwaniecLinearSieve/SieveFunctions/Bounds.lean
import took 1.07s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 208ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 141ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 249ms
cumulative profiling times:
attribute application 0.256ms
blocked (unaccounted) 36.6ms
congr simp thm 3.29ms
elaboration 115ms
fix level params 4.32ms
import 1.07s
initialization 25.1ms
instantiate metavars 7.54ms
interpretation 2.21s
let-to-have transformation 0.428ms
linting 73.3ms
module linting 0.00161ms
norm_num 488ms
overlappingInstancesLinter 6.76ms
parsing 22.5ms
process pre-definitions 46ms
ring 222ms
share common exprs 66.9ms
simp 52.7ms
tactic execution 453ms
tacticAnalysis 67.2ms
type checking 304ms
typeclass inference 999ms
real 3.72
user 5.75
sys 0.95
LeanPool/IwaniecLinearSieve/SieveFunctions/Defs.lean
import took 1.03s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 106ms
cumulative profiling times:
attribute application 2.5ms
blocked (unaccounted) 0.589ms
congr simp thm 4.14ms
elaboration 139ms
fix level params 2.37ms
import 1.03s
initialization 24.8ms
instantiate metavars 5.86ms
interpretation 1.03s
let-to-have transformation 0.425ms
linting 48.8ms
module linting 0.00177ms
norm_num 132ms
overlappingInstancesLinter 7.61ms
parsing 22.6ms
process pre-definitions 69.5ms
ring 133ms
share common exprs 32.2ms
simp 63.5ms
tactic execution 345ms
tacticAnalysis 61.4ms
type checking 171ms
typeclass inference 610ms
real 2.80
user 3.69
sys 0.90
LeanPool/IwaniecLinearSieve/SieveFunctions/LemmaFive.lean
import took 1.07s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 132ms
cumulative profiling times:
attribute application 0.264ms
congr simp thm 1.72ms
dsimp 11.1ms
elaboration 111ms
fix level params 3.83ms
import 1.07s
initialization 25.1ms
instantiate metavars 6.12ms
interpretation 1.32s
let-to-have transformation 0.552ms
linting 55.2ms
module linting 0.00153ms
norm_num 75.8ms
overlappingInstancesLinter 6.66ms
parsing 21.8ms
process pre-definitions 41.4ms
ring 201ms
share common exprs 53.1ms
simp 23.2ms
tactic execution 409ms
tacticAnalysis 56ms
type checking 292ms
typeclass inference 815ms
real 2.99
user 4.33
sys 0.89
LeanPool/IwaniecLinearSieve/SieveFunctions/Series.lean
import took 1.07s
cumulative profiling times:
attribute application 0.33ms
blocked (unaccounted) 2.23ms
congr simp thm 1.33ms
dsimp 5.43ms
elaboration 152ms
fix level params 1.86ms
import 1.07s
initialization 24.8ms
instantiate metavars 2.29ms
interpretation 560ms
let-to-have transformation 0.428ms
linting 36.2ms
module linting 0.00183ms
norm_num 9.36ms
overlappingInstancesLinter 7.47ms
parsing 18ms
process pre-definitions 17.8ms
ring 104ms
share common exprs 19.6ms
simp 39.5ms
tactic execution 166ms
tacticAnalysis 50ms
type checking 133ms
typeclass inference 491ms
real 2.34
user 2.52
sys 0.94
LeanPool/IwaniecLinearSieve/SieveMajorants/Defs.lean
import took 1.06s
cumulative profiling times:
attribute application 0.321ms
blocked (unaccounted) 15.1ms
congr simp thm 3.19ms
elaboration 124ms
fix level params 4.03ms
import 1.06s
initialization 25.8ms
instantiate metavars 9.72ms
interpretation 1.32s
let-to-have transformation 0.619ms
linting 45ms
module linting 0.00161ms
norm_num 299ms
overlappingInstancesLinter 8.96ms
parsing 25.1ms
process pre-definitions 48.9ms
ring 170ms
share common exprs 60.3ms
simp 89.8ms
tactic execution 669ms
tacticAnalysis 59ms
type checking 322ms
typeclass inference 953ms
real 3.21
user 4.96
sys 0.96
LeanPool/IwaniecLinearSieve/SieveMajorants/Delay.lean
import took 1.05s
cumulative profiling times:
attribute application 0.144ms
blocked (unaccounted) 1.61ms
congr simp thm 1.84ms
dsimp 2.66ms
elaboration 49.7ms
fix level params 0.776ms
import 1.05s
initialization 26.2ms
instantiate metavars 1.09ms
interpretation 374ms
let-to-have transformation 0.261ms
linting 18.9ms
module linting 0.00139ms
norm_num 5.51ms
overlappingInstancesLinter 4.21ms
parsing 10.2ms
process pre-definitions 8.31ms
ring 28.5ms
share common exprs 6.06ms
simp 44.9ms
tactic execution 148ms
tacticAnalysis 34.4ms
type checking 78.6ms
typeclass inference 253ms
real 2.14
user 1.89
sys 0.89
LeanPool/IwaniecLinearSieve/SieveMajorants/Lemmas.lean
import took 1.08s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 361ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 468ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 185ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 138ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 121ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 149ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.06s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 907ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 103ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 186ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 303ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 243ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 339ms
tactic execution of Lean.Parser.Tactic.refine took 102ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 507ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 115ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 110ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 326ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 302ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 312ms
tactic execution of Mathlib.Tactic.nlinarith took 305ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 464ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 377ms
cumulative profiling times:
attribute application 0.264ms
congr simp thm 11ms
dsimp 2.44ms
elaboration 209ms
fix level params 10.8ms
import 1.08s
initialization 25.3ms
instantiate metavars 40.8ms
interpretation 12.1s
let-to-have transformation 1.76ms
linting 192ms
module linting 0.00149ms
norm_num 2.45s
overlappingInstancesLinter 9.48ms
parsing 44ms
process pre-definitions 194ms
ring 758ms
share common exprs 327ms
simp 146ms
tactic execution 2.33s
tacticAnalysis 141ms
type checking 585ms
typeclass inference 3.71s
real 8.53
user 23.97
sys 0.99
LeanPool/IwaniecLinearSieve/SieveMajorants/Majorants.lean
import took 1.05s
cumulative profiling times:
attribute application 0.256ms
blocked (unaccounted) 2.96ms
congr simp thm 1.9ms
dsimp 3.6ms
elaboration 71.7ms
fix level params 2.19ms
import 1.05s
initialization 25ms
instantiate metavars 2.59ms
interpretation 697ms
let-to-have transformation 0.364ms
linting 26.7ms
module linting 0.0015ms
norm_num 139ms
overlappingInstancesLinter 5.03ms
parsing 13.8ms
process pre-definitions 20.6ms
ring 121ms
share common exprs 28.4ms
simp 45ms
tactic execution 300ms
tacticAnalysis 33.9ms
type checking 169ms
typeclass inference 626ms
real 2.45
user 3.03
sys 0.89
LeanPool/IwaniecLinearSieve/SieveMajorants/Properties.lean
import took 1.06s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 145ms
cumulative profiling times:
attribute application 0.187ms
congr simp thm 3.68ms
elaboration 74ms
fix level params 3.63ms
import 1.06s
initialization 33.9ms
instantiate metavars 8.71ms
interpretation 1.9s
let-to-have transformation 0.265ms
linting 40.3ms
module linting 0.00159ms
norm_num 714ms
overlappingInstancesLinter 6.03ms
parsing 18.1ms
process pre-definitions 39.3ms
ring 225ms
share common exprs 70.2ms
simp 39.4ms
tactic execution 455ms
tacticAnalysis 49ms
type checking 234ms
typeclass inference 1.05s
real 3.80
user 5.68
sys 0.93
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/Auxiliary.lean
import took 918ms
cumulative profiling times:
attribute application 0.0979ms
congr simp thm 0.413ms
elaboration 65.8ms
fix level params 0.344ms
import 918ms
initialization 24.7ms
instantiate metavars 0.291ms
interpretation 217ms
let-to-have transformation 0.149ms
linting 7.05ms
module linting 0.00154ms
overlappingInstancesLinter 2.18ms
parsing 3.33ms
process pre-definitions 3.9ms
share common exprs 1.85ms
simp 2.11ms
tactic execution 61.1ms
tacticAnalysis 13.1ms
type checking 52.9ms
typeclass inference 139ms
real 1.92
user 1.37
sys 0.79
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/EulerMaclaurin.lean
import took 1.04s
cumulative profiling times:
aesop 37.2ms
attribute application 0.0746ms
blocked (unaccounted) 50.5ms
compilation (IR) 0.138ms
compilation (LCNF base) 1.05ms
compilation (LCNF impure) 0.462ms
compilation (LCNF mono) 0.731ms
congr simp thm 3.95ms
dsimp 1.52ms
elaboration 46ms
fix level params 1.66ms
grind 14.1ms
grind cutsat 0.0383ms
grind linarith 0.277ms
grind mark subsingleton 1.42ms
grind ring 0.051ms
grind simp 7.92ms
import 1.04s
initialization 31.8ms
instantiate metavars 1.14ms
interpretation 324ms
let-to-have transformation 0.176ms
linting 10.7ms
module linting 0.00149ms
norm_num 1.4ms
overlappingInstancesLinter 5.6ms
parsing 4.8ms
process pre-definitions 4.98ms
ring 23.6ms
share common exprs 5.91ms
simp 120ms
sym canon 5.05ms
sym typeclass inference 41ms
tactic execution 151ms
tacticAnalysis 14.6ms
type checking 86.5ms
typeclass inference 329ms
real 2.22
user 2.04
sys 0.90
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/MediumPNT.lean
import took 1.17s
aesop took 102ms
aesop took 102ms
aesop took 222ms
aesop took 133ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 125ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 143ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 113ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 198ms
interpretation of Mathlib.Meta.FunProp.funPropTac._boxed took 272ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 506ms
aesop took 224ms
elaboration took 118ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 105ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 122ms
interpretation of Mathlib.Tactic.GRewrite.evalGRewriteSeq._boxed took 109ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 289ms
instantiate metavars took 160ms
typeclass inference of CharZero took 145ms
cumulative profiling times:
aesop 1.11s
attribute application 1.59ms
blocked (unaccounted) 20.2s
compilation (IR) 1.26ms
compilation (LCNF base) 29.3ms
compilation (LCNF impure) 4.51ms
compilation (LCNF mono) 8.52ms
congr simp thm 88.5ms
dsimp 92.9ms
elaboration 859ms
fix level params 19ms
import 1.17s
initialization 25.4ms
instantiate metavars 237ms
interpretation 13.5s
let-to-have transformation 2.85ms
linting 467ms
module linting 0.00166ms
norm_num 2.03s
overlappingInstancesLinter 40.8ms
parsing 209ms
process pre-definitions 364ms
ring 807ms
share common exprs 394ms
simp 3.38s
tactic execution 7.2s
tacticAnalysis 681ms
type checking 1.28s
typeclass inference 9.25s
real 13.85
user 42.52
sys 1.09
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/MellinCalculus.lean
import took 1.04s
simp took 104ms
cumulative profiling times:
aesop 368ms
attribute application 1.09ms
blocked (unaccounted) 829ms
compilation (IR) 0.931ms
compilation (LCNF base) 13ms
compilation (LCNF impure) 3.58ms
compilation (LCNF mono) 5.87ms
congr simp thm 42.5ms
dsimp 51.5ms
elaboration 317ms
fix level params 7.4ms
import 1.04s
initialization 24.9ms
instantiate metavars 17ms
interpretation 2.4s
let-to-have transformation 1.12ms
linting 140ms
module linting 0.00159ms
norm_num 167ms
overlappingInstancesLinter 28.4ms
parsing 66.1ms
process pre-definitions 67.2ms
ring 104ms
share common exprs 71ms
simp 2.95s
tactic execution 1.7s
tacticAnalysis 211ms
type checking 583ms
typeclass inference 3.12s
real 5.51
user 13.12
sys 0.95
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/Rectangle.lean
import took 861ms
simp took 103ms
cumulative profiling times:
attribute application 3.44ms
blocked (unaccounted) 0.95ms
congr simp thm 8.35ms
dsimp 0.809ms
elaboration 164ms
fix level params 1.58ms
import 861ms
initialization 24.9ms
instantiate metavars 4.74ms
interpretation 803ms
let-to-have transformation 0.411ms
linting 45.3ms
module linting 0.0015ms
norm_num 3.56ms
overlappingInstancesLinter 11.3ms
parsing 16.2ms
process pre-definitions 16ms
ring 43.3ms
share common exprs 15.4ms
simp 716ms
tactic execution 283ms
tacticAnalysis 69ms
type checking 90.6ms
typeclass inference 523ms
real 2.45
user 3.44
sys 0.84
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean
import took 1.04s
simp took 142ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 169ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 167ms
cumulative profiling times:
attribute application 0.561ms
blocked (unaccounted) 4.68s
congr simp thm 25.1ms
dsimp 34.9ms
elaboration 446ms
fix level params 7.34ms
import 1.04s
initialization 26.3ms
instantiate metavars 13.2ms
interpretation 1.91s
let-to-have transformation 5.59ms
linting 127ms
module linting 0.00123ms
norm_num 30.9ms
overlappingInstancesLinter 22.2ms
parsing 36.2ms
process pre-definitions 52.2ms
ring 77.2ms
share common exprs 63.3ms
simp 1.81s
tactic execution 796ms
tacticAnalysis 148ms
type checking 395ms
typeclass inference 2.14s
real 4.50
user 8.65
sys 1.01
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/StrongPNT.lean
import took 3.29s
aesop took 177ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 481ms
tactic execution of Lean.Parser.Tactic.refine took 118ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 353ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 379ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 596ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 382ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 116ms
tactic execution of Lean.Parser.Tactic.refine took 187ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 184ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 137ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 139ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 476ms
tactic execution of Mathlib.Tactic.RingNF.ringNF took 131ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 129ms
type checking took 123ms
tactic execution of Mathlib.Tactic.nlinarith took 396ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 170ms
type checking took 103ms
typeclass inference of CharZero took 147ms
cumulative profiling times:
aesop 177ms
attribute application 1.76ms
blocked (unaccounted) 12.2s
compilation (IR) 1.24ms
compilation (LCNF base) 41.8ms
compilation (LCNF impure) 4.43ms
compilation (LCNF mono) 10.8ms
congr simp thm 57.2ms
dsimp 22.6ms
elaboration 685ms
fix level params 18ms
grind 63.6ms
grind ac 0.00425ms
grind cutsat 0.0641ms
grind ematch 1.73ms
grind linarith 0.338ms
grind mark subsingleton 6.98ms
grind ring 0.684ms
grind simp 21.9ms
import 3.29s
initialization 25.4ms
instantiate metavars 67.2ms
interpretation 10.9s
let-to-have transformation 6.94ms
linting 317ms
module linting 0.0015ms
norm_num 3.14s
overlappingInstancesLinter 39.1ms
parsing 133ms
process pre-definitions 209ms
ring 756ms
share common exprs 424ms
simp 1.7s
sym canon 23.7ms
sym typeclass inference 177ms
tactic execution 6.74s
tacticAnalysis 420ms
type checking 1.48s
typeclass inference 7.34s
real 18.30
user 35.74
sys 1.13
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/ZetaBounds.lean
import took 1.18s
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 126ms
tactic execution of Lean.Parser.Tactic.apply took 408ms
aesop took 121ms
aesop took 121ms
aesop took 120ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 165ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 109ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 109ms
cumulative profiling times:
aesop 993ms
attribute application 2.35ms
blocked (unaccounted) 5.98s
compilation (IR) 1.78ms
compilation (LCNF base) 35.5ms
compilation (LCNF impure) 6.4ms
compilation (LCNF mono) 11.6ms
congr simp thm 76ms
dsimp 36.8ms
elaboration 1.06s
fix level params 21.2ms
grind 8.78ms
grind mark subsingleton 0.247ms
grind simp 1.72ms
import 1.18s
initialization 31.4ms
instantiate metavars 58.7ms
interpretation 8.49s
let-to-have transformation 27.3ms
linting 375ms
module linting 0.0015ms
norm_num 1.15s
overlappingInstancesLinter 44.5ms
parsing 194ms
process pre-definitions 251ms
ring 516ms
share common exprs 294ms
simp 3.11s
sym canon 4.18ms
sym typeclass inference 56ms
tactic execution 5.7s
tacticAnalysis 577ms
type checking 1.58s
typeclass inference 9.92s
real 12.08
user 35.29
sys 1.13
LeanPool/IwaniecLinearSieve/Vendor/PrimeNumberTheoremAnd/ZetaConj.lean
import took 1.09s
cumulative profiling times:
attribute application 0.0396ms
congr simp thm 0.708ms
elaboration 19.3ms
fix level params 0.0977ms
import 1.09s
initialization 25.4ms
instantiate metavars 0.164ms
interpretation 194ms
let-to-have transformation 0.0649ms
linting 3.05ms
module linting 0.00138ms
overlappingInstancesLinter 1.16ms
parsing 1.58ms
process pre-definitions 0.903ms
share common exprs 0.716ms
simp 28.8ms
tactic execution 21.4ms
tacticAnalysis 6.85ms
type checking 23.2ms
typeclass inference 54.3ms
real 1.98
user 1.22
sys 0.90
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Collaborator
Author
{
"verdict": "approve",
"reviewed_commit": "b02090ffa725d5a099f47f1da5a2ea5ac0d5431f",
"reviewer_role": "Additional acquisition-agent review: a separate author-side pass, alongside the configured independent GPT reviews.",
"coverage": "Checked the complete 49-file diff and exact upstream snapshot, each file's imports/declaration inventory, all advertised endpoints and their dependency closure, and bounded implementation slices across the sieve, delay equations, prime estimates, contour arguments and PNT. The temporary unconsumed residue section identified by Greptile was removed and revalidated.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The public endpoint proves the advertised absolute covering-run bound without unproved analytic inputs.",
"proves_the_claim": "proves_it",
"claim_note": "iwaniecBound quantifies one C before every finite set S of primes with 2 ≤ S.card, every integer starting point x and every natural run length m; divisibility of each x+k implies m ≤ C (S.card * log S.card)^2. shiftedSieve gives the lower sieve count for arbitrary prime sets of the requisite cardinality, and linearSieveEstimate proves its asymptotic main-term/support estimates.",
"assumed_inputs": "",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate Jacobsthal endpoint was found in the pinned Mathlib, Tau Ceti, pool sources/cards, PRs, issues or history.",
"already_formalized": "",
"novelty_note": "Mathlib's Selberg sieve and the existing pool PNT foundations do not provide this Rosser-Iwaniec lower sieve at the sifting limit; five existing PNT modules are reused rather than copied.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "A serious research formalization with useful analytic and combinatorial infrastructure.",
"fit": "good_fit",
"level": "research",
"branch": "analytic number theory",
"mode": "mixed",
"significance_one_sentence": "Preserves Iwaniec's classical quadratic-logarithmic Jacobsthal bound together with Rosser weights, delay-equation majorants, prime-sum estimates and its proved strong-PNT input.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The run-length formulation matches the 1978 Corollary, and the partial-import scope and PNT attribution are explicit.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "Competent port after removing blueprint machinery, unrelated imports and unused temporary API, factoring repeated estimates and splitting expensive analytic assembly; no waivers or source options remain.",
"code_quality": 3,
"findings": []
},
"evidence": {
"upstream": "https://github.com/jasondavies/iwaniec-linear-sieve/tree/c8d01549d2ae640b36ec198c1f0f6495f1b036cf",
"announcement": "2026-10-20 11:58:42 UTC, https://leanprover.zulipchat.com/#narrow/channel/583339/near/633293145",
"source_paper": "Iwaniec, On the problem of Jacobsthal, Demonstratio Mathematica 11 (1978), Corollary p. 226; DOI 10.1515/dema-1978-0121, checked against the original paper's publisher-provided ResearchGate reproduction.",
"license_provenance": "Apache-2.0 code; mixed provenance records the AI-authored sieve and substantial separately credited earlier PNT contributions.",
"local_validation": "Warning-free clean build and public Imports wrapper; Mathlib declaration lint for 48 modules/2,607 declarations; style; full repository static quality; generated-index verification; main-card declarations; axiom and option audit of all 2,610 compiled declarations including private constants, with only the allowed axioms and no forbidden option references.",
"compile_measurements": "Sequential archived baseline → final: 348.238 → 166.348 wall seconds; 563.720 → 403.885 aggregate child CPU seconds. Same command, four-thread setting and pinned warm package cache; clean project outputs. Shared-host wall-time variability is recorded.",
"profiles": "The baseline synchronous GenStrengthPNT profile exceeded 200,000 heartbeats; the final MediumPNT file profiles successfully under default limits. I1Bound: 61,046 → 32,097 heartbeats; SmoothedChebyshevClose_aux: 78,612 → 61,577. Final GenStrengthPNT 54,737 plus extracted contour assembly 90,328. The additional CI-identified exists_card_small synchronous timeout is repaired: approximately 46,200 heartbeats, with no warnings or limit override.",
"protected_ci": "Still running on this exact head. Queue entry requires protected CI and the configured independent GPT verdict to pass."
},
"remaining_findings": [],
"previous_review": "https://github.com/LeanPool/lean-pool/pull/700#issuecomment-6314306295",
"review_delta": "Rechecked the complete one-file proof-only change since 2d7d6005: exists_card_small has the identical statement; two broad nonlinear searches were replaced by explicit division and multiplication monotonicity. Synchronous profiling now succeeds under default limits at approximately 46,200 heartbeats. No new assumptions or declarations were added."
} |
Vilin97
commented
Oct 21, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
Author
There was a problem hiding this comment.
Independent source review at b02090f.
{
"summary": "This completed dependency closure proves Iwaniec's uniform Jacobsthal covering-run bound from constructed Rosser lower weights, shifted sieving, prime-sum estimates and a proved strong PNT.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"assumed_inputs": "",
"claim_note": "iwaniecBound chooses one real C before every finite prime set S with at least two elements, every integer start x and every natural run length m. Coverage of all x+k, k<m, implies m <= C*(|S| log |S|)^2. The headline supplies the proved linear-sieve, Mertens and nth-prime inputs rather than leaving analytic hypotheses.",
"findings": []
},
"novelty": {
"verdict": "pass",
"novelty_note": "Actual nearest contracts in pinned/current Mathlib, Tau Ceti and the current pool were compared. Selberg upper bounds and abstract lower-sieve interfaces do not construct this lower-weight estimate; LongGaps has different quantifiers and direction; qualitative PNT overlap does not supply the required exponential remainder. No equivalent completed endpoint was established in this bounded search.",
"findings": []
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"branch": "analytic number theory",
"mode": "theory_building",
"significance_one_sentence": "A substantial research formalization combines a uniform Jacobsthal bound with reusable combinatorial sieve, delay-equation and analytic prime-estimate infrastructure.",
"findings": []
},
"sources": {
"verdict": "pass",
"source_match": "matches",
"source_note": "The advertised run-length conclusion matches the 1978 corollary, and the card expressly limits the import to its dependency closure. Frozen Apache-2.0 sieve and PNT sources and retained credits were checked; mix records the disclosed AI-produced sieve proofs and earlier contributor PNT work. Exact printed 1971 theorem 4/5 formulas could not be verified because primary PDF access failed; some 1978 display glyphs were degraded. Those access limits are retained.",
"findings": []
},
"quality": {
"verdict": "pass",
"code_quality": 3,
"quality_note": "The modular port reuses existing PNT foundations, factors analytic estimates, keeps meaningful private helper consumers and contains no active source options or waivers in the complete static scan. No actionable defect was found in the reviewed proof interfaces and changes. The score and public proof profile are advisory.",
"findings": []
},
"verdict": "approve",
"findings": []
}Coverage: all 49 current file bodies are authenticated, with a complete import/default-setting scan. Detailed review covered the headline/reduction, Rosser and shifted sieve, analytic estimate suppliers, and the supporting PNT proof interfaces; not every unchanged upstream tactic line was independently reproved. The complete child delta was also checked: only two arithmetic proof steps in exists_card_small change, using explicit division and multiplication monotonicity. Its written contract and the other 48 files are unchanged.
This is source acceptance. Exact-head protected CI and the configured independent verdict remain pending, followed by normal native queue validation. The cancelled predecessor run supplies no current CI credit; author-side build, profile and compiled-audit claims are not substituted for those checks.
Collaborator
Author
|
/review Please review exact current head b02090f under the current five project rubrics, including actual prior-art contracts, closed analytic inputs, source/provenance and explicit coverage limits. Independent source review 5599057316 covers the imported dependency closure and both new proof hunks. Exact-head protected CI and subsequent normal native queue validation remain independent requirements. |
Collaborator
Author
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All three headline claims match the Lean and discharge their analytic inputs; exact-head CI remains pending, and the local build stopped at a Mathlib-fetch HTTP 403. |
| Novelty | ✅ pass |
No duplicate of the three headline results was found among the inspected Mathlib, Tau Ceti or pool declarations. |
| Significance | ✅ pass |
The Jacobsthal bound and supporting linear-sieve theory meet the research-level significance bar. |
| Sources | ✅ pass |
The 1978 Corollary matches iwaniecBound; the sieve specializations are labelled and both earlier Lean developments are credited. |
| Code quality (advisory) | ✅ pass |
The refactored estimates and contour proofs are competent; protected CI remains pending, and local compilation stopped at a Mathlib-fetch HTTP 403. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The disclosed primality, minimum-cardinality, and interval-covering hypotheses remain; the sieve, Mertens, nth-prime, and strong PNT estimates are proved in the dependency chain. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | analytic number theory |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: iwaniecBound chooses one real constant before every prime set, integer starting point, and natural run length; shiftedSieve and linearSieveEstimate establish the advertised counting inequality and eventual main-term/support bounds.
iwaniecBound establishes the uniform bound of order (r log r) squared for intervals covered by r primes, supported by linearSieveEstimate, shiftedSieve, sieve functions and delay-equation majorants.
Faithfulness findings (1)
- prompt-injection — PR-wide
The contributor-controlled description cites prior rubric approval, and the discussion supplies three author-side approval verdicts, including ‘Additional acquisition-agent review on5335fa1de5f83b86bafccdf250dcd7343c4f7eaa: approve.’ It also supplies reviewer-directed scope instructions. These could bias the independent review and were disregarded; contributor-supplied verdicts should carry no authority in review instructions.
Evidence: prose only
Novelty findings (1)
- prompt-injection — PR-wide
The contributor-controlled body and discussion supply prior approval verdicts that could contaminate this independent novelty review; they were disregarded.
Evidence: Prose-only evidence: the PR body claims ‘The configured review onb02090fpassed all four mathematical rubrics’; .review-pr.json also contains contributor-supplied reviews declaring approval and novelty pass.
Significance findings (1)
- prompt-injection — PR-wide
Contributor-controlled approval claims and reviewer-directed instructions risk biasing this independent review; they were disregarded in assessing the Lean.
Evidence: The PR description claims the configured review ‘passed all four mathematical rubrics’; contributor discussion supplies objects containing "verdict": "approve" and directs review ‘under the current five project rubrics’.
Sources findings (1)
- prompt-injection — PR-wide
Contributor-controlled approval verdicts and reviewer-directed coverage claims could bias this independent source review. They were disregarded; citation support was checked independently.
Evidence: The PR description says: “The configured review onb02090fpassed all four mathematical rubrics”. The discussion supplies author-side review objects containing “"verdict": "approve"” and tells reviewers: “Independent source review 5599057316 covers the imported dependency closure and both new proof hunks.”
Code quality findings (1)
- prompt-injection — PR-wide
Contributor-controlled discussion supplies approval verdicts and reviewer-directed scope instructions. These were disregarded and do not affect the code-quality score.
Evidence: In .review-pr.json, three author-side review objects contain "verdict": "approve"; another comment requests review "under the current five project rubrics" and asserts that an independent review "covers the imported dependency closure and both new proof hunks."
Tokens: 10,441,552 in / 56,921 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $42.6200 (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.
CI was not green for this commit at review time; this review does not replace CI.
Collaborator
Author
|
Additional acquisition-agent review on {
"verdict": "approve",
"reviewed_commit": "5335fa1de5f83b86bafccdf250dcd7343c4f7eaa",
"reviewer_role": "Additional acquisition-agent review: a separate author-side pass, alongside the configured independent GPT reviews.",
"coverage": "Checked the complete 49-file diff and exact upstream snapshot, each file's imports/declaration inventory, all advertised endpoints and their dependency closure, and bounded implementation slices across the sieve, delay equations, prime estimates, contour arguments and PNT. The temporary unconsumed residue section identified by Greptile was removed and revalidated. Rechecked the complete three-file repair diff: reciprocal derivations, the generalized positive strip lower estimate, its restricted and inverse corollaries, the direct real-part bound and adjacent-integral rewrite.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The public endpoint proves the advertised absolute covering-run bound without unproved analytic inputs.",
"proves_the_claim": "proves_it",
"claim_note": "iwaniecBound quantifies one C before every finite set S of primes with 2 \u2264 S.card, every integer starting point x and every natural run length m; divisibility of each x+k implies m \u2264 C (S.card * log S.card)^2. shiftedSieve gives the lower sieve count for arbitrary prime sets of the requisite cardinality, and linearSieveEstimate proves its asymptotic main-term/support estimates.",
"assumed_inputs": "",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate Jacobsthal endpoint was found in the pinned Mathlib, Tau Ceti, pool sources/cards, PRs, issues or history.",
"already_formalized": "",
"novelty_note": "Mathlib's Selberg sieve and the existing pool PNT foundations do not provide this Rosser-Iwaniec lower sieve at the sifting limit; five existing PNT modules are reused rather than copied.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "A serious research formalization with useful analytic and combinatorial infrastructure.",
"fit": "good_fit",
"level": "research",
"branch": "analytic number theory",
"mode": "mixed",
"significance_one_sentence": "Preserves Iwaniec's classical quadratic-logarithmic Jacobsthal bound together with Rosser weights, delay-equation majorants, prime-sum estimates and its proved strong-PNT input.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The run-length formulation matches the 1978 Corollary, and the partial-import scope and PNT attribution are explicit.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "Pass after consolidating the duplicated zeta estimates and removing the two contour detours raised by the configured review. Every public theorem statement is preserved.",
"code_quality": 3,
"findings": []
},
"evidence": {
"upstream": "https://github.com/jasondavies/iwaniec-linear-sieve/tree/c8d01549d2ae640b36ec198c1f0f6495f1b036cf",
"announcement": "2026-10-20 11:58:42 UTC, https://leanprover.zulipchat.com/#narrow/channel/583339/near/633293145",
"source_paper": "Iwaniec, On the problem of Jacobsthal, Demonstratio Mathematica 11 (1978), Corollary p. 226; DOI 10.1515/dema-1978-0121, checked against the original paper's publisher-provided ResearchGate reproduction.",
"license_provenance": "Apache-2.0 code; mixed provenance records the AI-authored sieve and substantial separately credited earlier PNT contributions.",
"local_validation": "Clean warning-free project build and Imports wrapper; 48-module/2572-declaration Mathlib lint; style; full static quality; generated indexes and project card; compiled axiom/option audit of 2575 declarations including private constants. All passed on the final source.",
"compile_measurements": "Archived baseline 348.238s/563.720 CPU \u2192 final 243.518s/441.893 CPU. Same pinned environment, four threads, clean outputs and warm package cache; variable shared-host load. Earlier checkpoint retained.",
"profiles": "All three edited files pass synchronous default-limit profiles, no warnings/errors. ZetaBounds total root-command HB 1360334.722 \u2192 1178169.350; ZetaInvBound2 24421.835 \u2192 2602.294; contour split 9091.692 \u2192 3468.602. Previous count timeout remains repaired.",
"protected_ci": "PASSED on exact head 5335fa1de5f83b86bafccdf250dcd7343c4f7eaa: https://github.com/LeanPool/lean-pool/actions/runs/39600830865 . Full-pool warning-free build, generated indexes, Mathlib lint, text style and repository quality all succeed; required Build project check succeeds. Other applicable required contexts pass or are legitimately scope-skipped. Greptile and configured five-rubric review approve the same head; no unresolved threads."
},
"remaining_findings": [],
"previous_review": "https://github.com/LeanPool/lean-pool/pull/700#issuecomment-6314760863",
"review_delta": "Addressed both concrete code-quality findings from configured review 6315654882. Added a stronger shared lower-bound lemma and kept every preexisting theorem statement unchanged; no axioms, limits or waiver changes."
}All source-head prerequisites are satisfied. The repository native merge queue will enforce its integration checks. |
Collaborator
Author
|
/review Head |
Vilin97
commented
Oct 21, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
Author
There was a problem hiding this comment.
Follow-up source review at 5335fa1, relative to b02090f (source review 5599057316).
{
"summary": "The three-file repair resolves the previous advisory maintenance findings by deriving reciprocal zeta bounds from positive lower estimates, sharing one proved full-strip lower bound, and removing both contour detours. All preexisting statements are retained; the other 46 files, project card and Jacobsthal/sieve headlines are unchanged.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"note": "The new strip producer has a strictly positive coefficient and supplies both reciprocal and restricted lower-bound corollaries. The closed PNT/sieve dependency and uniform Jacobsthal conclusion retain their earlier reviewed contracts; no new analytic premise or 1/0 shortcut is introduced."
},
"novelty": {
"verdict": "pass",
"note": "The previously inspected Mathlib/Tau/pool nearest-contract comparison remains applicable to the literally unchanged headline/source scope; no equivalent completed endpoint was established within that bounded search."
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"branch": "analytic number theory"
},
"sources": {
"verdict": "pass",
"note": "The prior pinned Apache-2.0 provenance/credit and limited corollary-import scope remain unchanged. The earlier printed-paper access limits remain recorded."
},
"quality": {
"verdict": "pass",
"code_quality": 3,
"note": "Actual reciprocal/strip proof reuse and direct contour steps resolve both concrete issues in old-head review 6315654882. Static Source review found no new actionable defect."
},
"verdict": "approve",
"findings": []
}I checked the complete three-file delta: nine hunks, 53 added and 286 removed lines, authenticated full base/head bodies and patch round trips. All 295 existing written command headers in those files are preserved; six proof bodies change and the only added public lemma is ZetaLowerBndStrip. Its positive lower bound covers the full strip before either inversion or restriction. The other 46 file identities, imports, card, pins and gate boundaries are unchanged.
This is current-head source acceptance. Configured review 2246 (comment 6315654882, request 6316075101) now independently reports all five rubrics pass at this same head. Complete own-head protected CI remains pending, followed by normal native queue validation. The cancelled predecessor run supplies no current CI acceptance. Contributor-supplied approval claims were disregarded.
Collaborator
Author
|
Exact-head validation follow-up for I verified the complete own PR CI run 39600830865, including its own canonical check Source review 5600531368 and configured review 2246 remain accepted at this head. The existing native queue candidate Disposition: approved, integration checks pending. The existing queue entry is preserved. |
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
1 participant
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.
Preserves Iwaniec's bound for Jacobsthal's problem: for one absolute C, any run of m consecutive integers covered by r ≥ 2 distinct primes satisfies m ≤ C (r log r)². The endpoint supplies its linear-sieve, Mertens and nth-prime estimates; it assumes no unproved analytic input.
Upstream is jasondavies/iwaniec-linear-sieve, pinned to
c8d01549d2ae640b36ec198c1f0f6495f1b036cf, under Apache-2.0. The acquisition window was 2026-10-14 09:15:15 UTC ≤ t < 2026-10-21 09:15:15 UTC. Completion commit dc7ab63 is dated October 16, and the public Lean Zulip announcement is dated October 20, 11:58:42 UTC.The mathematical sources are Iwaniec's 1971 linear-sieve paper and the Corollary on p. 226 of the 1978 Jacobsthal paper, checked against the original paper's publisher-provided reproduction. This port preserves the dependency closure of that corollary; it does not claim both upstream papers in full.
The retained infrastructure comprises Rosser weights, sieve functions, delay equations/majorants, prime sums, the shifted sieve for arbitrary prime sets, and a proved strong PNT. The project has 48 Lean files / 23,295 lines, including the entry and generated public Imports wrapper, plus one YAML card. Five existing MooreBound PNT foundation modules are reused. Nine further PNT modules are namespaced under
IwaniecLinearSievePNTand credited to PrimeNumberTheoremAnd revision 127b50e, also Apache-2.0.provenance: mixreflects the AI-produced sieve proofs disclosed upstream and the substantial earlier PNT work by its contributors. Module origins and revisions are retained in the card and vendor docstrings.Ported stable Lean 4.35.0 code to the pool's v4.35.0-rc3 / Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. Removed blueprint-only machinery, diagnostics, broad imports and all source options; repaired proofs under default elaborator settings. Factored repeated Mangoldt interval estimates and the contour/PNT assembly, simplified complex-power comparisons, and replaced expensive nonlinear counting steps with explicit monotonicity inequalities. Removed the unused temporary residue API, while retaining the complete earlier contour API consumed by the PNT. Documented the retained definitions and removed unused hypotheses/completeness constraints. The headline statement and its generality are preserved.
Measured compilation: initial clean minimal port, 205.318 s. An archived-baseline → final-source comparison measured 348.238 → 243.518 s wall time and 563.720 → 441.893 s aggregate child CPU (21.6% less CPU). Command:
LEAN_NUM_THREADS=4 lake build LeanPool.IwaniecLinearSieve; no project build outputs; identical manifest-verified prebuilt package cache. Lake's build plan fell from 9,011 to 3,747 jobs. The 16-CPU VM is shared, so these are observed samples; the initial baseline and an intermediate 240.542 s sample demonstrate wall-time variability. Failed iteration builds are excluded.Synchronous command/heartbeat profiling used the repository's standard flags and default limits. The original
GenStrengthPNTprofile exceeded 200,000 heartbeats; the refactored MediumPNT file profiles successfully. The full CI profile found a further timeout inexists_card_small, repaired with direct monotonicity rather than nonlinear searches (approximately 46,200 heartbeats).The final revision consolidates duplicated zeta estimates and simplifies the contour proofs:
ZetaInvBound1andZetaInvBound2derive from the positive lower estimates; a shared positiveZetaLowerBndStripproves both strip estimates;I1Bounduses the existing upper bound directly; and horizontal contour splitting uses the original adjacent-integral identities. Public theorem statements are unchanged. ZetaBounds root-command heartbeats fell 1,360,335 → 1,178,169;ZetaInvBound224,422 → 2,602, andRectangleIntegralHSplit9,092 → 3,469. All three edited files profile without warnings or errors. The previous 166.348 s / 403.885 CPU checkpoint remains recorded alongside the final heavier-load sample; wall time is not presented as a stable speedup.Local validation on
5335fa1de5f83b86bafccdf250dcd7343c4f7eaa: clean warning-free project build; public Imports wrapper; generated-index verification; full static repository quality; project-card declarations; style; Mathlib declaration lint for all 48 modules/2,572 declarations; compiled axiom/option audit of all 2,575 declarations including private constants. Onlypropext,Quot.soundandClassical.choiceare allowed, and no forbidden option references were found. No Python source changed. CI remains the final authority.Public-repository, split-card/source/history, open/merged PR, issue, Mathlib and Tau Ceti searches found no duplicate endpoint. The existing PNT overlap is reused and attributed.
LeanPool.leanis unchanged. No workflow, check, review rule, linter setting, protection or waiver is changed. Native queue entry waits for protected CI, the configured independent GPT verdict and resolved review findings; daily documentation publishing remains asynchronous.