Repository navigation
Import simple zeros of the Riemann zeta function - #381
Merged
Merged
Conversation
Vilin97
force-pushed
the
codex/daily-import-zeta-zeros-2026-09-03
branch
from
September 3, 2026 10:30
7058439 to
8601900
Compare
Greptile SummaryThe PR imports the ZetaZeros formalization, registers its conditional headline result, and integrates the complete module closure into Lean Pool.
|
| Filename | Overview |
|---|---|
| LeanPool/ZetaZeros.lean | The project entry module now imports both Main and Hilbert.InnerReal, completing the previously missing focused import closure. |
| LeanPool/ZetaZeros/Main.lean | Defines the conditional headline proportion theorems and connects the imported supporting development. |
| LeanPool/ZetaZeros/Defs.lean | Introduces the zero-counting, admissibility, and explicit analytic-hypothesis vocabulary used by the headline results. |
| LeanPool/ZetaZeros/Hilbert/InnerReal.lean | Supplies the public inner-product symmetry results now reachable through the project entry module. |
| LeanPool/projects.yml | Registers the project entry module, source revision, provenance, and main declaration consistently with the imported formalization. |
| LeanPool.lean | Adds the ZetaZeros entry module and every constituent module to the repository-wide umbrella. |
Reviews (6): Last reviewed commit: "Merge branch 'main' into codex/daily-imp..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
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: 1,544 maxHeartbeats units across 33 files (7,539 added LOC). Sum of Count-heartbeats wall-clock total: 162.36 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.ZetaZeros.Hilbert.AlphaExpansion |
17.00 s |
LeanPool.ZetaZeros |
8.70 s |
LeanPool.ZetaZeros.MontgomeryTaylor.AffineKernel |
8.00 s |
LeanPool.ZetaZeros.MontgomeryTaylor.Evaluation |
7.20 s |
LeanPool.ZetaZeros.MontgomeryTaylor.Reduction |
6.00 s |
LeanPool.ZetaZeros.MontgomeryTaylor.TestFunction |
5.40 s |
LeanPool.ZetaZeros.Zeta.Basic |
5.10 s |
LeanPool.ZetaZeros.Zeta.OrderConj |
5.10 s |
LeanPool.ZetaZeros.Zeta.Finite |
4.80 s |
LeanPool.ZetaZeros.Numeric.MontgomeryTaylor |
4.40 s |
LeanPool.ZetaZeros.Zeta.Cutoff |
4.10 s |
LeanPool.ZetaZeros.MontgomeryTaylor.Basic |
4.10 s |
Per-file `lean --profile` output
LeanPool/ZetaZeros.lean
import took 2.15s
cumulative profiling times:
elaboration 0.211ms
import 2.15s
initialization 28.5ms
interpretation 222ms
linting 0.311ms
module linting 0.00135ms
overlappingInstancesLinter 0.515ms
parsing 0.0281ms
tacticAnalysis 1.87ms
real 3.11
user 1.76
sys 1.36
LeanPool/ZetaZeros/Defs.lean
import took 1.46s
cumulative profiling times:
attribute application 0.349ms
blocked (unaccounted) 1.83ms
elaboration 39.7ms
fix level params 0.0988ms
import 1.46s
initialization 29.2ms
instantiate metavars 0.179ms
interpretation 300ms
let-to-have transformation 0.118ms
linting 6.98ms
module linting 0.00134ms
overlappingInstancesLinter 4.37ms
parsing 8.14ms
process pre-definitions 4.96ms
share common exprs 0.501ms
tactic execution 0.253ms
tacticAnalysis 19.4ms
type checking 15.9ms
typeclass inference 68.4ms
real 2.44
user 1.55
sys 1.02
LeanPool/ZetaZeros/Hilbert/AlphaExpansion.lean
import took 1.6s
simp took 209ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 273ms
tactic execution of Lean.Parser.Tactic.solveByElim took 173ms
tactic execution of Lean.Parser.Tactic.solveByElim took 159ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 152ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 130ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 165ms
tactic execution of Mathlib.Tactic.nlinarith took 328ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 322ms
tactic execution of Mathlib.Tactic.nlinarith took 387ms
tactic execution of Mathlib.Tactic.nlinarith took 724ms
tactic execution of Mathlib.Tactic.nlinarith took 403ms
tactic execution of Mathlib.Tactic.nlinarith took 523ms
tactic execution of Mathlib.Tactic.nlinarith took 895ms
cumulative profiling times:
attribute application 2.45ms
congr simp thm 88ms
dsimp 50.1ms
elaboration 1.08s
fix level params 25.9ms
import 1.6s
initialization 38ms
instantiate metavars 53.3ms
interpretation 4.77s
let-to-have transformation 4.44ms
linting 457ms
module linting 0.00128ms
norm_num 255ms
overlappingInstancesLinter 52ms
parsing 277ms
process pre-definitions 221ms
ring 360ms
share common exprs 193ms
simp 2.99s
tactic execution 9.64s
tacticAnalysis 833ms
type checking 1.99s
typeclass inference 10s
real 11.17
user 34.17
sys 1.41
LeanPool/ZetaZeros/Hilbert/Basis.lean
import took 1.59s
cumulative profiling times:
attribute application 3.72ms
blocked (unaccounted) 6.48ms
elaboration 59.4ms
fix level params 0.126ms
import 1.59s
initialization 35ms
instantiate metavars 0.0759ms
interpretation 263ms
let-to-have transformation 0.0635ms
linting 4.96ms
module linting 0.00118ms
overlappingInstancesLinter 1.73ms
parsing 3.55ms
process pre-definitions 2.03ms
share common exprs 0.613ms
tacticAnalysis 12.4ms
type checking 65.6ms
typeclass inference 143ms
real 2.70
user 1.76
sys 1.04
LeanPool/ZetaZeros/Hilbert/Defs.lean
import took 1.46s
cumulative profiling times:
attribute application 0.238ms
blocked (unaccounted) 0.319ms
congr simp thm 0.805ms
elaboration 20.9ms
fix level params 0.333ms
import 1.46s
initialization 35.5ms
instantiate metavars 0.217ms
interpretation 303ms
let-to-have transformation 0.0643ms
linting 4.22ms
module linting 0.00121ms
norm_num 2.67ms
overlappingInstancesLinter 3.01ms
parsing 4.71ms
process pre-definitions 3.71ms
ring 20.7ms
share common exprs 2.89ms
simp 11.2ms
tactic execution 5.24ms
tacticAnalysis 13.6ms
type checking 26.4ms
typeclass inference 35.5ms
real 2.42
user 1.51
sys 1.03
LeanPool/ZetaZeros/Hilbert/Dimensions.lean
import took 1.6s
cumulative profiling times:
attribute application 0.0574ms
congr simp thm 2.98ms
elaboration 21.7ms
fix level params 0.66ms
import 1.6s
initialization 30.6ms
instantiate metavars 0.882ms
interpretation 323ms
let-to-have transformation 0.13ms
linting 4.43ms
module linting 0.00128ms
overlappingInstancesLinter 6.22ms
parsing 4.56ms
process pre-definitions 2.37ms
share common exprs 2.39ms
simp 166ms
tactic execution 169ms
tacticAnalysis 16.5ms
type checking 39.4ms
typeclass inference 406ms
real 2.91
user 2.38
sys 1.07
LeanPool/ZetaZeros/Hilbert/FIdentity.lean
import took 1.45s
cumulative profiling times:
attribute application 0.0465ms
blocked (unaccounted) 1.11ms
congr simp thm 1.18ms
elaboration 22.2ms
fix level params 0.383ms
import 1.45s
initialization 28.6ms
instantiate metavars 0.891ms
interpretation 299ms
let-to-have transformation 0.0558ms
linting 11.5ms
module linting 0.00126ms
norm_num 1.8ms
overlappingInstancesLinter 3.82ms
parsing 7.44ms
process pre-definitions 3.26ms
ring 27.2ms
share common exprs 3.7ms
simp 28.1ms
tactic execution 70.1ms
tacticAnalysis 20.7ms
type checking 24.7ms
typeclass inference 39.6ms
real 2.44
user 1.63
sys 1.01
LeanPool/ZetaZeros/Hilbert/InnerReal.lean
import took 1.44s
cumulative profiling times:
attribute application 0.0383ms
congr simp thm 0.358ms
elaboration 11.1ms
fix level params 0.0714ms
import 1.44s
initialization 29.7ms
instantiate metavars 0.114ms
interpretation 247ms
let-to-have transformation 0.0358ms
linting 3.1ms
module linting 0.00134ms
norm_num 0.76ms
overlappingInstancesLinter 1.08ms
parsing 3.23ms
process pre-definitions 0.82ms
share common exprs 0.495ms
tactic execution 43.9ms
tacticAnalysis 11ms
type checking 11.5ms
typeclass inference 43.1ms
real 2.41
user 1.45
sys 1.01
LeanPool/ZetaZeros/Hilbert/InnerRealL2.lean
import took 1.59s
cumulative profiling times:
attribute application 0.0234ms
congr simp thm 0.408ms
elaboration 13.2ms
fix level params 0.102ms
import 1.59s
initialization 36.7ms
instantiate metavars 0.246ms
interpretation 301ms
let-to-have transformation 0.0317ms
linting 3.04ms
module linting 0.00134ms
norm_num 0.413ms
overlappingInstancesLinter 3.42ms
parsing 2.55ms
process pre-definitions 1.05ms
ring 7.91ms
share common exprs 1.57ms
simp 2.75ms
tactic execution 16ms
tacticAnalysis 10.4ms
type checking 8.79ms
typeclass inference 51.9ms
real 2.59
user 1.57
sys 1.09
LeanPool/ZetaZeros/Hilbert/Integrals.lean
import took 1.43s
cumulative profiling times:
attribute application 0.121ms
congr simp thm 2.68ms
elaboration 32.1ms
fix level params 0.404ms
import 1.43s
initialization 29.2ms
instantiate metavars 0.644ms
interpretation 296ms
let-to-have transformation 0.0808ms
linting 9.02ms
module linting 0.0016ms
norm_num 0.76ms
overlappingInstancesLinter 2.13ms
parsing 7.45ms
process pre-definitions 3.08ms
ring 16.2ms
share common exprs 4.96ms
simp 52.2ms
tactic execution 95.9ms
tacticAnalysis 19ms
type checking 33.5ms
typeclass inference 198ms
real 2.50
user 1.81
sys 1.03
LeanPool/ZetaZeros/Hilbert/L2.lean
import took 1.59s
cumulative profiling times:
attribute application 0.341ms
blocked (unaccounted) 0.307ms
congr simp thm 1.67ms
dsimp 2.95ms
elaboration 36.5ms
fix level params 0.531ms
import 1.59s
initialization 37.6ms
instantiate metavars 0.483ms
interpretation 355ms
let-to-have transformation 0.158ms
linting 10.1ms
module linting 0.00136ms
norm_num 2.49ms
overlappingInstancesLinter 3.15ms
parsing 9.54ms
process pre-definitions 7.4ms
ring 28.9ms
share common exprs 6.33ms
simp 39.3ms
tactic execution 123ms
tacticAnalysis 27.2ms
type checking 47.4ms
typeclass inference 232ms
real 2.67
user 2.09
sys 1.08
LeanPool/ZetaZeros/Hilbert/Subspaces.lean
import took 1.58s
cumulative profiling times:
attribute application 0.15ms
congr simp thm 0.307ms
elaboration 48.4ms
fix level params 0.189ms
import 1.58s
initialization 28.6ms
instantiate metavars 0.111ms
interpretation 265ms
let-to-have transformation 0.149ms
linting 4.66ms
module linting 0.00117ms
overlappingInstancesLinter 2.69ms
parsing 4.49ms
process pre-definitions 6.23ms
share common exprs 1.07ms
simp 1.65ms
tactic execution 8.28ms
tacticAnalysis 13.1ms
type checking 25.7ms
typeclass inference 148ms
real 2.65
user 1.72
sys 1.05
LeanPool/ZetaZeros/Hilbert/Symmetry.lean
import took 1.44s
cumulative profiling times:
attribute application 0.118ms
blocked (unaccounted) 0.301ms
congr simp thm 1.76ms
elaboration 11.4ms
fix level params 0.355ms
import 1.44s
initialization 30.5ms
instantiate metavars 0.334ms
interpretation 302ms
let-to-have transformation 0.0384ms
linting 4.8ms
module linting 0.00117ms
norm_num 1.94ms
overlappingInstancesLinter 1.63ms
parsing 3.11ms
process pre-definitions 2.57ms
ring 7.44ms
share common exprs 3.58ms
simp 47.3ms
tactic execution 29.7ms
tacticAnalysis 10.4ms
type checking 32.5ms
typeclass inference 148ms
real 2.44
user 1.69
sys 1.01
LeanPool/ZetaZeros/Hilbert/SymmetryL2.lean
import took 1.59s
cumulative profiling times:
attribute application 0.0254ms
congr simp thm 0.857ms
dsimp 26.6ms
elaboration 20.6ms
fix level params 0.123ms
import 1.59s
initialization 35.4ms
instantiate metavars 0.152ms
interpretation 313ms
let-to-have transformation 0.0601ms
linting 5.79ms
module linting 0.00134ms
norm_num 0.276ms
overlappingInstancesLinter 1.67ms
parsing 2.76ms
process pre-definitions 3.38ms
ring 4.97ms
share common exprs 0.99ms
simp 44.3ms
tactic execution 24.5ms
tacticAnalysis 13.5ms
type checking 49.4ms
typeclass inference 125ms
real 2.70
user 1.79
sys 1.08
LeanPool/ZetaZeros/Main.lean
import took 1.59s
cumulative profiling times:
attribute application 0.133ms
blocked (unaccounted) 2.15ms
congr simp thm 0.651ms
dsimp 9.2ms
elaboration 24.8ms
fix level params 1.09ms
import 1.59s
initialization 34.6ms
instantiate metavars 1.07ms
interpretation 513ms
let-to-have transformation 0.0895ms
linting 12.3ms
module linting 0.0014ms
norm_num 149ms
overlappingInstancesLinter 2.31ms
parsing 10.3ms
process pre-definitions 10.2ms
ring 62.7ms
share common exprs 14.4ms
simp 6.86ms
tactic execution 140ms
tacticAnalysis 23ms
type checking 78.3ms
typeclass inference 365ms
real 2.84
user 2.55
sys 1.09
LeanPool/ZetaZeros/Meta/Attr.lean
import took 654ms
cumulative profiling times:
attribute application 0.156ms
blocked (unaccounted) 2.23ms
compilation (IR) 0.433ms
compilation (LCNF base) 8.38ms
compilation (LCNF impure) 1.76ms
compilation (LCNF mono) 4.1ms
do element elaborator 4.58ms
elaboration 2.89ms
fix level params 0.0207ms
import 654ms
initialization 30.8ms
instantiate metavars 0.011ms
interpretation 4.03ms
let-to-have transformation 0.0399ms
linting 0.834ms
module linting 0.00141ms
parsing 1.03ms
process pre-definitions 0.649ms
share common exprs 0.102ms
tactic execution 0.0618ms
type checking 0.533ms
typeclass inference 3.76ms
real 1.28
user 0.62
sys 0.68
LeanPool/ZetaZeros/MontgomeryTaylor/AffineKernel.lean
import took 1.45s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 120ms
aesop took 101ms
cumulative profiling times:
aesop 160ms
attribute application 0.0631ms
compilation (IR) 0.0825ms
compilation (LCNF base) 0.862ms
compilation (LCNF impure) 0.327ms
compilation (LCNF mono) 0.617ms
congr simp thm 6.88ms
elaboration 35.5ms
fix level params 1.07ms
import 1.45s
initialization 28.8ms
instantiate metavars 2.78ms
interpretation 1s
let-to-have transformation 0.0816ms
linting 19.3ms
module linting 0.00129ms
norm_num 359ms
overlappingInstancesLinter 3.07ms
parsing 21ms
process pre-definitions 18.7ms
ring 77.8ms
share common exprs 27.1ms
simp 1.35s
tactic execution 522ms
tacticAnalysis 51.4ms
type checking 94.4ms
typeclass inference 745ms
real 5.88
user 5.58
sys 1.02
LeanPool/ZetaZeros/MontgomeryTaylor/Basic.lean
import took 1.45s
cumulative profiling times:
attribute application 0.0307ms
congr simp thm 0.605ms
elaboration 5.84ms
fix level params 0.195ms
import 1.45s
initialization 36.5ms
instantiate metavars 0.376ms
interpretation 348ms
let-to-have transformation 0.022ms
linting 2.59ms
module linting 0.00125ms
norm_num 87.6ms
overlappingInstancesLinter 1.13ms
parsing 3.19ms
process pre-definitions 2.08ms
ring 12.6ms
share common exprs 3.63ms
simp 3.3ms
tactic execution 48.2ms
tacticAnalysis 10.8ms
type checking 15.4ms
typeclass inference 83.5ms
real 2.68
user 1.71
sys 1.01
LeanPool/ZetaZeros/MontgomeryTaylor/Evaluation.lean
import took 1.44s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 151ms
cumulative profiling times:
aesop 129ms
attribute application 0.0141ms
compilation (IR) 0.104ms
compilation (LCNF base) 0.899ms
compilation (LCNF impure) 0.324ms
compilation (LCNF mono) 0.566ms
congr simp thm 4.09ms
elaboration 11.5ms
fix level params 0.653ms
import 1.44s
initialization 29.2ms
instantiate metavars 1.01ms
interpretation 848ms
let-to-have transformation 0.0137ms
linting 8.37ms
module linting 0.00138ms
norm_num 193ms
overlappingInstancesLinter 1.48ms
parsing 8.28ms
process pre-definitions 10.6ms
ring 38.8ms
share common exprs 16.3ms
simp 633ms
tactic execution 290ms
tacticAnalysis 26.4ms
type checking 46.3ms
typeclass inference 414ms
real 4.73
user 3.79
sys 0.98
LeanPool/ZetaZeros/MontgomeryTaylor/Integrability.lean
import took 1.43s
cumulative profiling times:
attribute application 0.0593ms
congr simp thm 0.282ms
elaboration 44.2ms
fix level params 0.106ms
import 1.43s
initialization 36ms
instantiate metavars 0.125ms
interpretation 266ms
let-to-have transformation 0.0718ms
linting 3.38ms
module linting 0.00124ms
overlappingInstancesLinter 2.04ms
parsing 3.93ms
process pre-definitions 1.85ms
share common exprs 0.894ms
simp 0.823ms
tactic execution 29ms
tacticAnalysis 11.8ms
type checking 19.1ms
typeclass inference 78.8ms
real 2.37
user 1.52
sys 0.99
LeanPool/ZetaZeros/MontgomeryTaylor/Reduction.lean
import took 1.45s
cumulative profiling times:
attribute application 0.0694ms
blocked (unaccounted) 1.07ms
congr simp thm 3.42ms
dsimp 4.09ms
elaboration 43.3ms
fix level params 1.42ms
import 1.45s
initialization 29ms
instantiate metavars 3.37ms
interpretation 1.26s
let-to-have transformation 0.118ms
linting 27.6ms
module linting 0.00143ms
norm_num 570ms
overlappingInstancesLinter 3.71ms
parsing 30.6ms
process pre-definitions 24.7ms
ring 80.7ms
share common exprs 21.4ms
simp 50ms
tactic execution 723ms
tacticAnalysis 65.4ms
type checking 112ms
typeclass inference 824ms
real 4.11
user 4.69
sys 1.04
LeanPool/ZetaZeros/MontgomeryTaylor/TestFunction.lean
import took 1.45s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 120ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 363ms
cumulative profiling times:
attribute application 0.104ms
blocked (unaccounted) 74.2ms
congr simp thm 2.09ms
dsimp 1.31ms
elaboration 28.9ms
fix level params 0.81ms
import 1.45s
initialization 28.8ms
instantiate metavars 0.961ms
interpretation 1.05s
let-to-have transformation 0.118ms
linting 10.1ms
module linting 0.00144ms
norm_num 198ms
overlappingInstancesLinter 2.46ms
parsing 13.9ms
process pre-definitions 13ms
ring 38.9ms
share common exprs 9.86ms
simp 97.5ms
tactic execution 181ms
tacticAnalysis 34ms
type checking 64.8ms
typeclass inference 475ms
real 3.42
user 3.23
sys 1.04
LeanPool/ZetaZeros/Numeric/MontgomeryTaylor.lean
import took 1.27s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 132ms
cumulative profiling times:
attribute application 0.419ms
congr simp thm 2.96ms
elaboration 47.2ms
fix level params 2.33ms
import 1.27s
initialization 29.4ms
instantiate metavars 2.16ms
interpretation 1.01s
let-to-have transformation 0.209ms
linting 13.7ms
module linting 0.00129ms
norm_num 309ms
overlappingInstancesLinter 4.57ms
parsing 16.3ms
process pre-definitions 20.5ms
ring 62.7ms
share common exprs 27.4ms
simp 266ms
tactic execution 202ms
tacticAnalysis 33.4ms
type checking 163ms
typeclass inference 865ms
real 2.87
user 3.97
sys 0.95
LeanPool/ZetaZeros/Zeta/Asymptotics.lean
import took 1.44s
cumulative profiling times:
attribute application 0.0422ms
congr simp thm 0.706ms
dsimp 8.82ms
elaboration 9.74ms
fix level params 0.28ms
import 1.44s
initialization 29ms
instantiate metavars 0.42ms
interpretation 337ms
let-to-have transformation 0.0453ms
linting 3.53ms
module linting 0.00122ms
norm_num 38.4ms
overlappingInstancesLinter 1.97ms
parsing 3.48ms
process pre-definitions 3.19ms
ring 16.9ms
share common exprs 2.89ms
simp 3.37ms
tactic execution 31.6ms
tacticAnalysis 10.9ms
type checking 22.5ms
typeclass inference 65.8ms
real 2.45
user 1.61
sys 1.01
LeanPool/ZetaZeros/Zeta/Basic.lean
import took 1.44s
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 133ms
cumulative profiling times:
attribute application 0.656ms
congr simp thm 7.85ms
dsimp 2.98ms
elaboration 83.1ms
fix level params 1.65ms
import 1.44s
initialization 28.5ms
instantiate metavars 1.9ms
interpretation 780ms
let-to-have transformation 0.296ms
linting 30.2ms
module linting 0.00117ms
norm_num 105ms
overlappingInstancesLinter 5.45ms
parsing 23.8ms
process pre-definitions 17.8ms
ring 53.5ms
share common exprs 16ms
simp 262ms
tactic execution 406ms
tacticAnalysis 52.9ms
type checking 148ms
typeclass inference 989ms
real 3.08
user 4.00
sys 1.04
LeanPool/ZetaZeros/Zeta/Cutoff.lean
import took 1.47s
cumulative profiling times:
attribute application 0.042ms
congr simp thm 0.863ms
elaboration 4.75ms
fix level params 0.152ms
import 1.47s
initialization 33.5ms
instantiate metavars 0.224ms
interpretation 282ms
let-to-have transformation 0.0246ms
linting 2.7ms
module linting 0.00145ms
norm_num 43.4ms
overlappingInstancesLinter 0.827ms
parsing 2.02ms
process pre-definitions 1.17ms
ring 6.43ms
share common exprs 1.86ms
simp 34.9ms
tactic execution 20.1ms
tacticAnalysis 7ms
type checking 13.7ms
typeclass inference 73.2ms
real 2.57
user 1.58
sys 1.02
LeanPool/ZetaZeros/Zeta/Defs.lean
import took 1.45s
cumulative profiling times:
attribute application 0.245ms
blocked (unaccounted) 2.21ms
elaboration 27.7ms
fix level params 0.0613ms
import 1.45s
initialization 33.2ms
instantiate metavars 0.099ms
interpretation 258ms
let-to-have transformation 0.0589ms
linting 4.35ms
module linting 0.00116ms
overlappingInstancesLinter 2.82ms
parsing 5.17ms
process pre-definitions 3.27ms
share common exprs 0.314ms
tacticAnalysis 11ms
type checking 22.9ms
typeclass inference 53.1ms
real 2.39
user 1.48
sys 1.00
LeanPool/ZetaZeros/Zeta/Finite.lean
import took 1.59s
cumulative profiling times:
attribute application 0.0455ms
congr simp thm 0.364ms
elaboration 3.08ms
fix level params 0.0955ms
import 1.59s
initialization 35ms
instantiate metavars 0.158ms
interpretation 271ms
let-to-have transformation 0.0251ms
linting 2.1ms
module linting 0.00126ms
norm_num 0.681ms
overlappingInstancesLinter 1.74ms
parsing 2.22ms
process pre-definitions 0.907ms
ring 5.01ms
share common exprs 1.09ms
simp 2.71ms
tactic execution 24.2ms
tacticAnalysis 7.49ms
type checking 6.04ms
typeclass inference 23.4ms
real 2.55
user 1.54
sys 1.07
LeanPool/ZetaZeros/Zeta/Kernel.lean
import took 1.59s
typeclass inference of CharZero took 255ms
typeclass inference of CharZero took 243ms
cumulative profiling times:
attribute application 0.778ms
blocked (unaccounted) 1.41s
congr simp thm 12.5ms
dsimp 64.3ms
elaboration 223ms
fix level params 5.85ms
import 1.59s
initialization 28.4ms
instantiate metavars 11.3ms
interpretation 1.7s
let-to-have transformation 0.817ms
linting 96.4ms
module linting 0.0014ms
norm_num 225ms
overlappingInstancesLinter 10.8ms
parsing 79.6ms
process pre-definitions 66.4ms
ring 146ms
share common exprs 75.5ms
simp 476ms
tactic execution 1.51s
tacticAnalysis 161ms
type checking 505ms
typeclass inference 2.87s
real 4.81
user 9.25
sys 1.15
LeanPool/ZetaZeros/Zeta/Mass.lean
import took 1.46s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 106ms
cumulative profiling times:
attribute application 0.0461ms
blocked (unaccounted) 0.0933ms
congr simp thm 0.695ms
elaboration 8.45ms
fix level params 0.273ms
import 1.46s
initialization 38.8ms
instantiate metavars 0.166ms
interpretation 384ms
let-to-have transformation 0.0307ms
linting 2.99ms
module linting 0.00124ms
norm_num 34.8ms
overlappingInstancesLinter 1.19ms
parsing 4.05ms
process pre-definitions 2.65ms
ring 9.58ms
share common exprs 3.09ms
simp 4.39ms
tactic execution 64.8ms
tacticAnalysis 10.5ms
type checking 21.8ms
typeclass inference 126ms
real 2.73
user 1.74
sys 1.04
LeanPool/ZetaZeros/Zeta/OrderConj.lean
import took 1.48s
tactic execution of Lean.Parser.Tactic.exact took 130ms
cumulative profiling times:
attribute application 0.202ms
blocked (unaccounted) 325ms
congr simp thm 5.48ms
dsimp 18.5ms
elaboration 53ms
fix level params 1.15ms
import 1.48s
initialization 28.9ms
instantiate metavars 2.78ms
interpretation 498ms
let-to-have transformation 0.189ms
linting 28ms
module linting 0.00111ms
norm_num 38.8ms
overlappingInstancesLinter 4.59ms
parsing 20.5ms
process pre-definitions 12.2ms
ring 35.9ms
share common exprs 10.2ms
simp 129ms
tactic execution 483ms
tacticAnalysis 49.7ms
type checking 133ms
typeclass inference 720ms
real 2.92
user 3.26
sys 1.05
LeanPool/ZetaZeros/Zeta/Proportion.lean
import took 1.45s
cumulative profiling times:
attribute application 0.0363ms
congr simp thm 0.571ms
dsimp 10.8ms
elaboration 22.4ms
fix level params 0.442ms
import 1.45s
initialization 38.6ms
instantiate metavars 0.677ms
interpretation 461ms
let-to-have transformation 0.0731ms
linting 9.94ms
module linting 0.00136ms
norm_num 42.7ms
overlappingInstancesLinter 1.95ms
parsing 4.1ms
process pre-definitions 4.98ms
ring 18ms
share common exprs 4.71ms
simp 8.34ms
tactic execution 36.2ms
tacticAnalysis 14.1ms
type checking 32.6ms
typeclass inference 161ms
real 2.58
user 1.90
sys 1.01
LeanPool/ZetaZeros/Zeta/Transfer.lean
import took 1.59s
cumulative profiling times:
attribute application 0.142ms
congr simp thm 3.43ms
elaboration 30.1ms
fix level params 0.675ms
import 1.59s
initialization 28.6ms
instantiate metavars 1.43ms
interpretation 378ms
let-to-have transformation 0.108ms
linting 16.2ms
module linting 0.0013ms
norm_num 2.37ms
overlappingInstancesLinter 2.8ms
parsing 10.2ms
process pre-definitions 6.02ms
ring 25.4ms
share common exprs 6.06ms
simp 91.8ms
tactic execution 111ms
tacticAnalysis 27.1ms
type checking 40.6ms
typeclass inference 172ms
real 2.64
user 2.07
sys 1.08
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All four headline declarations prove the card’s claims, with their analytic and finite-multiset assumptions explicitly disclosed. |
| Novelty | ✅ pass |
The four headline results are not already formalized in Mathlib or any listed pool project. |
| Significance | ✅ pass |
This is a research-level analytic number theory project with named asymptotic bounds and a substantial supporting Hilbert-space and zeta-zero development. |
| Sources | ✅ pass |
The citations and attributions are internally consistent, but the exact 67.25% and 83.625% results are not quoted from Lamzouri’s paper and remain unverifiable from the diff alone. |
| Code quality (advisory) | ✅ pass |
The analytic, Hilbert-space, and transfer arguments are separated into coherent modules and reusable lemmas, with no material maintenance debt evident. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The proportion theorems assume RiemannVonMangoldt and PairCorrelation; the abstract bounds assume IsAdmissible and IsConjInvariant. The card discloses all of these, and its nonemptiness restriction is stronger than Lean requires. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | analytic number theory |
| Mode | theory_building |
| Code quality | 4 / 5 |
Statement check: The two proportion theorems give strict eventual lower bounds of 0.6725 and 0.83625 for the stated zero-count ratios, while the two abstract theorems give the claimed kernel bounds for every admissible function and conjugation-invariant finite multiset, including the empty case.
The project proves the conditional eventual bounds 0.6725 for simple critical-line zeros and 0.83625 for distinct zeros, while developing the finite-multiset Hilbert-space inequality, kernel construction, multiplicity symmetries, and certified Montgomery–Taylor estimate used in those results.
Tokens: 641,773 in / 9,282 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $1.7437
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.
Vilin97
force-pushed
the
codex/daily-import-zeta-zeros-2026-09-03
branch
from
September 3, 2026 11:14
8601900 to
aad1243
Compare
Vilin97
force-pushed
the
codex/daily-import-zeta-zeros-2026-09-03
branch
from
September 3, 2026 11:49
aad1243 to
1819eb9
Compare
Collaborator
Author
|
/review |
Collaborator
Author
|
Fixed the remaining import-closure finding on exact head |
Contributor
|
LLM review skipped: Lean Action CI conclusion was |
Collaborator
Author
|
/review |
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.
Summary
Import the mathematical closure of AxiomMath/ZetaZeros at
4bcaf70e544506c311d83a5a5b143a134b9fc5f7, corresponding to Lamzouri, A new proof that more than 2/3 of the zeros of the Riemann zeta function are simple and on the critical line.The source commit landed at 2026-09-02 15:08:03 UTC, inside the automation's exact discovery window
[2026-08-27T09:01:38Z, 2026-09-03T09:01:38Z). Repository history, open/closed issues and PRs,LeanPool/projects.yml, and existing project paths/cards showed no prior ZetaZeros import.The imported headline theorems are deliberately recorded as conditional:
ZetaZeros.simple_proportion_d4proves the eventual lower bound0.6725assuming the formalized Riemann--von Mangoldt and pair-correlation hypotheses.ZetaZeros.distinct_proportion_d5proves the eventual lower bound0.83625under the same explicit hypotheses.The import does not claim to prove those analytic inputs. It does include the supporting Hilbert-space optimization, zero-set finiteness, symmetry/multiplicity, kernel, asymptotic, and transfer arguments needed by the two results.
Scope and provenance
LeanPool/projects.ymlZetaZeros; imports rewritten underLeanPool.ZetaZerosLeanPool/projects.yml; the repository's separation guard requires the generatedNOTICErefresh to remain outside this content PRTrust and source fidelity
#print axiomsfor the two headline results and three representative intermediate theorems reports exactly:No
sorry,admit,axiom,unsafe,native_decide, project-local options, mutable dependencies, or external binaries were introduced.Optimization
Before editing, a dependency-warm clean build of the imported closure took 34.27 s (3,611 Lake jobs). After removing 18 redundant direct imports, reducing the project umbrella to
Main, and extracting the oversized initial-span proof into a private helper, two clean builds took 29.72 s and 30.72 s (3,609 jobs): a 10.4--13.3% wall-time improvement.The hottest module,
Hilbert/AlphaExpansion.lean, improved from 5.93 s / 2,535,716 KiB to 4.23 s / 2,522,620 KiB in isolated direct builds (28.7% faster, 0.5% lower peak RSS). The concurrent whole-closure peak sample was noisy and increased from 2,203,076 KiB to about 4,169,500 KiB, so no aggregate memory improvement is claimed.Validation
lake build LeanPool.ZetaZeros(warning-free)lake build LeanPool(9,496 jobs)scripts/ci/build-challenges.sh(4,055 jobs; only the three expected existing challengesorrynotices)lake exe runLinter LeanPool.ZetaZeroslake exe lint-style LeanPool.ZetaZeroslake exe runLinter LeanPoollake exe lint-style LeanPoollake exe mk_all --checkcd python && uv run python -m lean_pool.quality --repo ..cd python && uv run --group test pytest -q -k 'not test_repository_notice_is_current'(316 passed; the deselected repository-currentness test requests the intentionally separated generatedNOTICErefresh)git diff --checkThe required five independent rubric reviews (faithfulness, novelty, significance, sources, and code quality) are left for the repository workflow on this PR.