Repository navigation
Import selberg-sieve4 formalization - #86
Conversation
Proof profile (new / modified Lean files)
This is the parallel build wall clock and is the compile-time answer for this PR. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 1,012 maxHeartbeats units across 17 files (2,840 added LOC). Sum of Count-heartbeats wall-clock total: 54.54 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.SelbergSieve4.Applications.PrimeCountingUpperBound |
5.70 s |
LeanPool.SelbergSieve4.Selberg |
5.20 s |
LeanPool.SelbergSieve4.Applications.BrunTitchmarsh |
4.20 s |
LeanPool.SelbergSieve4.SieveLemmas |
4.10 s |
LeanPool.SelbergSieve4.AuxResults |
4.00 s |
LeanPool.SelbergSieve4.ForMathlib.Basic |
3.60 s |
LeanPool.SelbergSieve4.UpperBoundSieve |
2.70 s |
LeanPool.SelbergSieve4.Tactic.AesopDiv |
2.70 s |
LeanPool.SelbergSieve4.ForArithmeticFunction |
2.50 s |
LeanPool.SelbergSieve4.MainResults |
2.50 s |
LeanPool.SelbergSieve4.ForMathlib |
2.40 s |
LeanPool.SelbergSieve4.ForMathlib.ProdsAntidiagonal |
2.30 s |
Per-file `lean --profile` output
LeanPool/SelbergSieve4.lean
import took 2.16s
cumulative profiling times:
elaboration 0.143ms
import 2.16s
initialization 28.4ms
interpretation 214ms
linting 0.222ms
parsing 0.0439ms
real 3.05
user 1.81
sys 1.26
LeanPool/SelbergSieve4/Applications.lean
import took 2.2s
cumulative profiling times:
elaboration 0.161ms
import 2.2s
initialization 27.8ms
interpretation 210ms
linting 0.198ms
parsing 0.0326ms
real 3.08
user 1.79
sys 1.31
LeanPool/SelbergSieve4/Applications/BrunTitchmarsh.lean
import took 2.19s
cumulative profiling times:
aesop 28.6ms
attribute application 0.229ms
blocked (unaccounted) 0.655ms
compilation (IR) 0.191ms
compilation (LCNF base) 2.23ms
compilation (LCNF impure) 0.882ms
compilation (LCNF mono) 2.4ms
congr simp thm 12.9ms
elaboration 134ms
fix level params 2ms
import 2.19s
initialization 28.2ms
instantiate metavars 4.39ms
interpretation 1.11s
let-to-have transformation 0.364ms
linting 36.4ms
norm_num 219ms
parsing 19.6ms
process pre-definitions 18.8ms
ring 98.4ms
share common exprs 27.3ms
simp 291ms
tactic execution 517ms
type checking 193ms
typeclass inference 1.26s
real 4.68
user 5.49
sys 1.35
LeanPool/SelbergSieve4/Applications/PrimeCountingUpperBound.lean
import took 2.18s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 128ms
cumulative profiling times:
aesop 33.8ms
attribute application 0.91ms
blocked (unaccounted) 9.89ms
compilation (IR) 1.43ms
compilation (LCNF base) 22.8ms
compilation (LCNF impure) 7.89ms
compilation (LCNF mono) 22.4ms
congr simp thm 28.4ms
dsimp 1.66ms
elaboration 246ms
fix level params 5.11ms
import 2.18s
initialization 27.8ms
instantiate metavars 15ms
interpretation 2.58s
let-to-have transformation 0.898ms
linting 108ms
norm_num 423ms
parsing 59.9ms
process pre-definitions 54.6ms
ring 171ms
share common exprs 63.5ms
simp 810ms
tactic execution 1.23s
type checking 416ms
typeclass inference 3.42s
real 5.78
user 11.14
sys 1.45
LeanPool/SelbergSieve4/AuxResults.lean
import took 2.19s
cumulative profiling times:
attribute application 0.31ms
blocked (unaccounted) 9.9ms
compilation (IR) 0.549ms
compilation (LCNF base) 10.8ms
compilation (LCNF impure) 3.16ms
compilation (LCNF mono) 8.67ms
congr simp thm 9.54ms
elaboration 100ms
fix level params 2.05ms
import 2.19s
initialization 27.7ms
instantiate metavars 3.51ms
interpretation 1.17s
let-to-have transformation 0.362ms
linting 32ms
norm_num 46.9ms
parsing 20.8ms
process pre-definitions 17.2ms
ring 31.3ms
share common exprs 11.9ms
simp 362ms
tactic execution 405ms
type checking 130ms
typeclass inference 1.59s
real 4.34
user 5.49
sys 1.32
LeanPool/SelbergSieve4/ForArithmeticFunction.lean
import took 1.61s
cumulative profiling times:
elaboration 0.0815ms
import 1.61s
initialization 27.6ms
interpretation 144ms
linting 0.111ms
parsing 0.00227ms
real 2.40
user 1.42
sys 0.99
LeanPool/SelbergSieve4/ForMathlib.lean
import took 2.15s
cumulative profiling times:
elaboration 0.143ms
import 2.15s
initialization 27.8ms
interpretation 205ms
linting 0.208ms
parsing 0.033ms
real 3.03
user 1.76
sys 1.29
LeanPool/SelbergSieve4/ForMathlib/Basic.lean
import took 2.17s
cumulative profiling times:
attribute application 0.0218ms
congr simp thm 0.483ms
elaboration 8.38ms
fix level params 0.173ms
import 2.17s
initialization 27.7ms
instantiate metavars 0.0274ms
interpretation 261ms
let-to-have transformation 0.0344ms
linting 2.45ms
norm_num 0.294ms
parsing 0.882ms
process pre-definitions 0.581ms
share common exprs 0.556ms
simp 10.1ms
tactic execution 9.64ms
type checking 7.82ms
typeclass inference 73.5ms
real 3.17
user 1.97
sys 1.27
LeanPool/SelbergSieve4/ForMathlib/ProdsAntidiagonal.lean
import took 1.29s
cumulative profiling times:
attribute application 0.0875ms
compilation (IR) 0.0454ms
compilation (LCNF base) 0.427ms
compilation (LCNF impure) 0.212ms
compilation (LCNF mono) 0.22ms
congr simp thm 0.493ms
elaboration 11.9ms
fix level params 0.0507ms
import 1.29s
initialization 28.2ms
instantiate metavars 0.0627ms
interpretation 159ms
let-to-have transformation 0.0566ms
linting 1.82ms
parsing 1.52ms
process pre-definitions 0.477ms
share common exprs 0.144ms
simp 3.8ms
tactic execution 0.533ms
type checking 1.13ms
typeclass inference 8.47ms
real 2.05
user 1.22
sys 0.88
LeanPool/SelbergSieve4/MainResults.lean
import took 2.18s
cumulative profiling times:
attribute application 0.0417ms
elaboration 13.2ms
fix level params 0.0816ms
import 2.18s
initialization 27.6ms
instantiate metavars 0.0894ms
interpretation 244ms
let-to-have transformation 0.0653ms
linting 1.7ms
norm_num 0.238ms
parsing 1.49ms
process pre-definitions 0.624ms
ring 5.9ms
share common exprs 0.577ms
tactic execution 3.48ms
type checking 5.72ms
typeclass inference 53.3ms
real 3.18
user 1.92
sys 1.29
LeanPool/SelbergSieve4/Selberg.lean
import took 2.18s
cumulative profiling times:
aesop 214ms
attribute application 3.71ms
blocked (unaccounted) 789ms
compilation (IR) 4.17ms
compilation (LCNF base) 202ms
compilation (LCNF impure) 19.2ms
compilation (LCNF mono) 56.7ms
congr simp thm 9.34ms
dsimp 16.8ms
elaboration 146ms
fix level params 2.51ms
import 2.18s
initialization 27.9ms
instantiate metavars 5.18ms
interpretation 1.38s
let-to-have transformation 0.711ms
linting 50.3ms
norm_num 14.2ms
parsing 27.6ms
process pre-definitions 43.7ms
ring 69.6ms
share common exprs 22.5ms
simp 379ms
tactic execution 658ms
type checking 147ms
typeclass inference 1.15s
real 5.37
user 6.25
sys 1.36
LeanPool/SelbergSieve4/SieveLemmas.lean
import took 2.2s
cumulative profiling times:
aesop 141ms
attribute application 4.09ms
blocked (unaccounted) 348ms
compilation (IR) 3.19ms
compilation (LCNF base) 146ms
compilation (LCNF impure) 14.8ms
compilation (LCNF mono) 43.3ms
congr simp thm 7.26ms
dsimp 18.4ms
elaboration 159ms
fix level params 1.88ms
import 2.2s
initialization 28ms
instantiate metavars 4.48ms
interpretation 1.03s
let-to-have transformation 0.677ms
linting 37.3ms
norm_num 13.4ms
parsing 26.3ms
process pre-definitions 32.5ms
ring 50.7ms
share common exprs 16.5ms
simp 83.4ms
tactic execution 366ms
type checking 126ms
typeclass inference 674ms
real 4.43
user 4.60
sys 1.35
LeanPool/SelbergSieve4/Tactic.lean
import took 1.62s
cumulative profiling times:
elaboration 0.135ms
import 1.62s
initialization 27.6ms
interpretation 152ms
linting 0.227ms
parsing 0.0313ms
real 2.40
user 1.39
sys 1.03
LeanPool/SelbergSieve4/Tactic/AesopDiv.lean
import took 1.6s
cumulative profiling times:
attribute application 1.36ms
blocked (unaccounted) 123ms
compilation (IR) 0.522ms
compilation (LCNF base) 17.6ms
compilation (LCNF impure) 3.03ms
compilation (LCNF mono) 6.2ms
congr simp thm 0.613ms
elaboration 69ms
fix level params 0.302ms
import 1.6s
initialization 28ms
instantiate metavars 0.245ms
interpretation 346ms
let-to-have transformation 0.35ms
linting 11.5ms
norm_num 0.22ms
parsing 15.5ms
process pre-definitions 5.55ms
ring 3ms
share common exprs 1.37ms
simp 11.2ms
tactic execution 13.6ms
type checking 11.1ms
typeclass inference 51.3ms
real 2.64
user 1.80
sys 1.03
LeanPool/SelbergSieve4/Tactic/AesopInit.lean
import took 907ms
cumulative profiling times:
attribute application 0.0309ms
compilation (IR) 0.112ms
compilation (LCNF base) 2.79ms
compilation (LCNF impure) 0.612ms
compilation (LCNF mono) 1.25ms
elaboration 0.259ms
fix level params 0.00678ms
import 907ms
initialization 27.6ms
instantiate metavars 0.00563ms
interpretation 20.2ms
let-to-have transformation 0.0061ms
linting 0.145ms
parsing 0.0437ms
process pre-definitions 0.242ms
share common exprs 0.0217ms
type checking 0.151ms
typeclass inference 0.704ms
real 1.52
user 0.85
sys 0.69
LeanPool/SelbergSieve4/Tactic/Multiplicativity.lean
import took 196ms
cumulative profiling times:
elaboration 0.0571ms
import 196ms
initialization 27.9ms
interpretation 3.01ms
linting 0.0621ms
parsing 0.0046ms
real 0.74
user 0.37
sys 0.39
LeanPool/SelbergSieve4/UpperBoundSieve.lean
import took 1.63s
cumulative profiling times:
attribute application 0.295ms
blocked (unaccounted) 0.227ms
compilation (IR) 0.0735ms
compilation (LCNF base) 0.935ms
compilation (LCNF impure) 0.395ms
compilation (LCNF mono) 0.633ms
congr simp thm 0.869ms
elaboration 16.3ms
fix level params 0.0222ms
import 1.63s
initialization 28ms
instantiate metavars 0.0275ms
interpretation 179ms
let-to-have transformation 0.0191ms
linting 1.36ms
parsing 2.21ms
process pre-definitions 0.857ms
share common exprs 0.0946ms
simp 0.433ms
type checking 3.05ms
typeclass inference 4.21ms
real 2.45
user 1.45
sys 1.04
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | graduate |
| Branch | analytic number theory |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a formalized Selberg sieve with standard prime-counting applications, which is a recognizable piece of graduate-level analytic number theory.
Tokens: 45,072 in / 731 out · Tier: standard · Cost: $0.2473
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
|
/profile |
1 similar comment
|
/profile |
|
Deterministic partial-port audit flags this PR as a lower-confidence partial import against the registered upstream source. Compared with The registered main declarations appear to be present, so I would not treat this like the stronger headline-result omissions above without a human look. Still, it is over the 10% LOC tolerance and should be resolved by either porting the omitted files or explicitly documenting/narrowing the project scope. This is the failure mode automated in #110. |
|
Follow-up on the lower-confidence partial-port audit: I checked the omitted upstream files directly. The registered headline results in this PR are present, and the missing upstream files are not clean Lean Pool imports as-is: |
|
/profile |
# Conflicts: # LeanPool/projects.yml
|
Follow-up audit for the lower-confidence partial-port flag: the main Selberg sieve results are present and registered ( Against current upstream So I agree with the earlier lower-confidence assessment: this is not a case where registered headline results were dropped. The missing upstream material is unfinished/non-admissible as Lean Pool content. Note: the flag labelled this as PR #85, but the Selberg sieve PR is #86; #85 is the zeta_3_irrational import. |
Imported from https://github.com/FLDutchmann/selberg-sieve4.
Slug:
selberg-sieve4Toolchain target:
leanprover/lean4:v4.30.0-rc2Branch:
import/selberg-sieve4(auto-generated byscripts/import-formalization.sh)Agent:
codexusinggpt-5.5at effortxhigh, exited with code0.Commits on this branch:
Opened automatically by
scripts/import-formalization.sh. Review the diff carefully before merging — the agent ran unattended.