Repository navigation
Import gradient-only acceleration under generalized smoothness - #693
Merged
Merged
Conversation
Collaborator
Author
|
Thorough source review — APPROVE at {
"review": "Acquisition source review, separate pass over the final import",
"head_sha": "6dfb3e682fdc9714fd88a179695f445b05399985",
"conclusion": "approve",
"reviewer_scope": "A separate review pass by the acquisition agent; the configured GPT review remains the independent verdict.",
"coverage": {
"upstream": "All 17 modules in the selected dependency closure, 2,605 upstream lines, inspected in bounded chunks; all endpoint declarations and transitive imports covered.",
"diff": "All 20 added files at this head, including the 19 Lean modules/wrappers and project YAML; all source edits beyond the mechanical port reviewed.",
"build_and_profiles": "Warning-free clean build, generated indexes, style, static quality, 516-declaration lint/trust checks, clean timing logs and command-heartbeat profiles inspected.",
"ci": "Content/non-content separation and both metadata/partial-import advisories have passed. Required Build project is still running through the configured Lean workflow. Documentation preflight, Python and workflow-lint jobs were skipped by their configured scope conditions."
},
"merge_eligibility": "Wait for required CI and configured independent reviews, resolve every material finding, then use normal protected queue validation. This source approval does not waive any gate or the infrastructure priority hold.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The card describes the actual generalized-smooth convex objective-gap and exact gradient-query guarantee.",
"proves_the_claim": "proves_it",
"claim_note": "SelfNormalized.result supplies one algorithm family from Public information, uniformly over positive target accuracy, with the stated ceiling/minimum budget; execute_gradient_oracle equates 2*N queries with N genuine accelerated steps.",
"assumed_inputs": "A complete real inner-product space; convexity; an everywhere differentiable exact gradient satisfying the Hessian-growth norm bound; an attained minimum; positive L0, R, Delta and epsilon, and nonnegative L1. These are disclosed in the card. Oracle correctness is required at every call and sample; no convergence claim is hidden in a structure field.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "The examined libraries do not contain the selected discrete generalized-smooth, gradient-only oracle-complexity endpoint.",
"already_formalized": "",
"novelty_note": "Mathlib gradient calculus and Tau Ceti norm_gradient_eq_norm_fderiv, maximal-slope-flow convergence and Moreau-Yosida existence statements do not provide this finite-query algorithm. The pool's ParameterFreeGradient project targets gradient-norm accuracy under global Lipschitz smoothness in finite-dimensional lp spaces, with a different oracle/model. Searches were bounded; this is a negative search finding, not an exhaustive equivalence proof.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a completed research-level convergence development with reusable mathematical and oracle-execution infrastructure.",
"fit": "good_fit",
"level": "research",
"branch": "convex optimization",
"mode": "theory_building",
"significance_one_sentence": "The formalization preserves a gradient-only accelerated bound under gradient-dependent Hessian growth, with explicit accounting, local gradient estimates, energy dissipation, charging and weighted inequalities.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The exact upstream formalization, license, completion commit and credited authors support the import's stated scope.",
"source_match": "matches",
"findings": []
},
"code_quality": {
"verdict": "pass",
"bottom_line": "The closure has short cohesive modules and explicit supporting lemmas; targeted import and arithmetic repairs substantially reduce compilation cost without changing the result.",
"code_quality": 3,
"findings": []
},
"engineering_checks": {
"algorithm_and_boundary_cases": "Checked the Delta<=epsilon zero-query return, L1=0 branch, positivity requirements, natural ceiling, both queries per step, and the choice of the smaller of two bounds for the same algorithm. Exact-gradient uniqueness makes execution independent of the oracle seeds; it does not assume an optimizer oracle or free function-value evaluations.",
"nonvacuity": "The assumptions admit ordinary smooth convex quadratics; no constructor or bundled predicate asserts descent, termination accuracy or the main convergence bound.",
"trust": "The existing axiom and compiled-declaration audits pass over all owned modules, including auxiliary/generated declarations, with only Classical.choice/propext/Quot.sound permitted. No prohibited mechanism, heartbeat override, suppression or gate edit is introduced.",
"attribution_and_scope": "Apache-2.0 source, upstream authors and AI proof provenance recorded. Only the selected mathematical closure is imported; unrelated upstream automation and third-party UI assets are absent. LeanPool.lean remains byte-identical.",
"compile": "Comparable clean builds: 47.81s -> 36.89s; max RSS 1,784,552 -> 1,529,120 KiB. The main accuracy proof's enclosing command profile falls 122,991 -> 22,077 heartbeats. No theorem statement or budget is weakened."
}
} |
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] No blocking issue was found in the metadata-only update, but external source checks remain unverified. SummaryThe update since the previous review only adds explicit parameter limits to the
Reviews (3) · Last reviewed commit: "docs: state gradient-descent positivity ..." · Reviewed by 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,163,421 maxHeartbeats units across 19 valid files (3,019 added LOC). Sum of Count-heartbeats wall-clock total: 160.66 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.LongTails.Proofs.GeneralizedAcceleratedEnergy |
5.40 s |
LeanPool.LongTails.Proofs.GeneralizedLogCharging |
4.50 s |
LeanPool.LongTails.Proofs.GeneralizedCharging |
4.30 s |
LeanPool.LongTails.Proofs.GdConvex |
4.30 s |
LeanPool.LongTails.Proofs.GeneralizedConvergence |
4.20 s |
LeanPool.LongTails.Template |
3.70 s |
LeanPool.LongTails.Proofs.Execution |
3.60 s |
LeanPool.LongTails.Proofs.GeneralizedMixedRate |
3.60 s |
LeanPool.LongTails.Proofs.DampedGeneralizedDynamics |
3.40 s |
LeanPool.LongTails.Setups.SmoothAndConvex |
3.30 s |
LeanPool.LongTails.Proofs.GeneralizedGradientStep |
2.90 s |
LeanPool.LongTails.Proofs.GeneralizedSelfNormalizedConvergence |
2.80 s |
Per-file `lean --profile` output
LeanPool/LongTails.lean
import took 2.71s
cumulative profiling times:
elaboration 0.193ms
import 2.71s
initialization 31.9ms
interpretation 207ms
linting 0.555ms
module linting 0.00139ms
overlappingInstancesLinter 0.433ms
parsing 0.0309ms
tacticAnalysis 2.6ms
real 3.69
user 1.29
sys 1.21
LeanPool/LongTails/Algorithms/DampedGeneralizedAccelerated.lean
import took 1.21s
cumulative profiling times:
attribute application 0.0831ms
blocked (unaccounted) 1.41ms
compilation (IR) 0.229ms
compilation (LCNF base) 1.43ms
compilation (LCNF impure) 1.08ms
compilation (LCNF mono) 1.77ms
congr simp thm 0.211ms
elaboration 61.1ms
fix level params 0.221ms
import 1.21s
initialization 31.5ms
instantiate metavars 0.125ms
interpretation 278ms
let-to-have transformation 3.42ms
linting 8.86ms
module linting 0.00176ms
overlappingInstancesLinter 5.58ms
parsing 7.01ms
process pre-definitions 6.69ms
share common exprs 0.588ms
simp 1.2ms
tactic execution 8.81ms
tacticAnalysis 22.7ms
type checking 18.1ms
typeclass inference 106ms
real 2.42
user 1.58
sys 1.01
LeanPool/LongTails/Algorithms/Gd.lean
import took 1.12s
cumulative profiling times:
attribute application 0.0101ms
elaboration 6.94ms
fix level params 0.0341ms
import 1.12s
initialization 30.1ms
instantiate metavars 0.0161ms
interpretation 213ms
let-to-have transformation 0.0215ms
linting 1.9ms
module linting 0.00153ms
overlappingInstancesLinter 2.28ms
parsing 1.26ms
process pre-definitions 0.91ms
share common exprs 0.116ms
tactic execution 0.696ms
tacticAnalysis 3.58ms
type checking 2.14ms
typeclass inference 26.8ms
real 2.08
user 1.15
sys 0.99
LeanPool/LongTails/Imports.lean
import took 1.14s
cumulative profiling times:
elaboration 0.116ms
import 1.14s
initialization 30.2ms
interpretation 189ms
linting 0.247ms
module linting 0.00136ms
overlappingInstancesLinter 0.122ms
parsing 0.00182ms
tacticAnalysis 0.478ms
real 2.06
user 1.14
sys 0.96
LeanPool/LongTails/Proofs/DampedGeneralizedDynamics.lean
import took 1.14s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 531ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 277ms
cumulative profiling times:
attribute application 0.315ms
compilation (IR) 0.106ms
compilation (LCNF base) 0.554ms
compilation (LCNF impure) 0.496ms
compilation (LCNF mono) 0.777ms
congr simp thm 6.7ms
dsimp 32.8ms
elaboration 285ms
fix level params 8.08ms
import 1.14s
initialization 35.8ms
instantiate metavars 8.91ms
interpretation 2.34s
let-to-have transformation 10.1ms
linting 92.8ms
module linting 0.00567ms
norm_num 274ms
overlappingInstancesLinter 18.6ms
parsing 38.1ms
process pre-definitions 38ms
ring 164ms
share common exprs 55.6ms
simp 267ms
tactic execution 448ms
tacticAnalysis 125ms
type checking 276ms
typeclass inference 1.79s
real 3.91
user 7.18
sys 1.01
LeanPool/LongTails/Proofs/DampedGeneralizedExecution.lean
import took 1.14s
cumulative profiling times:
attribute application 3.56ms
congr simp thm 1.48ms
elaboration 33.3ms
fix level params 0.371ms
import 1.14s
initialization 31ms
instantiate metavars 0.371ms
interpretation 263ms
let-to-have transformation 0.0897ms
linting 8.5ms
module linting 0.00172ms
norm_num 1.33ms
overlappingInstancesLinter 2.38ms
parsing 4.26ms
process pre-definitions 1.62ms
share common exprs 1.14ms
simp 4.49ms
tactic execution 54.1ms
tacticAnalysis 20.8ms
type checking 15.7ms
typeclass inference 42.4ms
real 2.22
user 1.41
sys 0.99
LeanPool/LongTails/Proofs/Execution.lean
import took 1.11s
cumulative profiling times:
attribute application 0.0771ms
congr simp thm 2.07ms
dsimp 1.43ms
elaboration 74.2ms
fix level params 1.47ms
import 1.11s
initialization 33.7ms
instantiate metavars 1.36ms
interpretation 287ms
let-to-have transformation 6.74ms
linting 13.5ms
module linting 0.00181ms
overlappingInstancesLinter 2.63ms
parsing 10.8ms
process pre-definitions 3.72ms
share common exprs 3.2ms
simp 22.2ms
tactic execution 76.6ms
tacticAnalysis 29.9ms
type checking 46.8ms
typeclass inference 70.4ms
real 2.20
user 1.57
sys 0.95
LeanPool/LongTails/Proofs/GdConvex.lean
import took 1.13s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 192ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 154ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 216ms
cumulative profiling times:
attribute application 0.0657ms
congr simp thm 9.78ms
dsimp 11.8ms
elaboration 76.1ms
fix level params 4.14ms
import 1.13s
initialization 32.3ms
instantiate metavars 4.93ms
interpretation 1.27s
let-to-have transformation 0.246ms
linting 39ms
module linting 0.00146ms
norm_num 109ms
overlappingInstancesLinter 6.31ms
parsing 15.1ms
process pre-definitions 20.4ms
ring 89.1ms
share common exprs 28.2ms
simp 256ms
tactic execution 337ms
tacticAnalysis 41.8ms
type checking 183ms
typeclass inference 1.44s
real 3.93
user 4.85
sys 1.00
LeanPool/LongTails/Proofs/GeneralizedAcceleratedEnergy.lean
import took 1.13s
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 383ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.11s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 411ms
cumulative profiling times:
attribute application 0.0213ms
congr simp thm 3.64ms
dsimp 9.16ms
elaboration 52.1ms
fix level params 3.23ms
import 1.13s
initialization 30.5ms
instantiate metavars 7.83ms
interpretation 2.64s
let-to-have transformation 1.71ms
linting 38.4ms
module linting 0.00161ms
norm_num 137ms
overlappingInstancesLinter 4.18ms
parsing 6.2ms
process pre-definitions 15.1ms
ring 88.2ms
share common exprs 32.1ms
simp 79ms
tactic execution 186ms
tacticAnalysis 23.7ms
type checking 96.4ms
typeclass inference 922ms
real 5.82
user 5.29
sys 0.97
LeanPool/LongTails/Proofs/GeneralizedCharging.lean
import took 671ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 108ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 173ms
cumulative profiling times:
attribute application 0.211ms
blocked (unaccounted) 24.1ms
compilation (IR) 0.462ms
compilation (LCNF base) 7.63ms
compilation (LCNF impure) 2.12ms
compilation (LCNF mono) 4.34ms
congr simp thm 14.7ms
elaboration 75.1ms
fix level params 1.54ms
import 671ms
initialization 30.4ms
instantiate metavars 3.59ms
interpretation 852ms
let-to-have transformation 0.95ms
linting 29.8ms
module linting 0.00143ms
norm_num 151ms
overlappingInstancesLinter 6.06ms
parsing 19.2ms
process pre-definitions 15.6ms
ring 61.2ms
share common exprs 17ms
simp 233ms
tactic execution 205ms
tacticAnalysis 53.9ms
type checking 100ms
typeclass inference 284ms
real 2.60
user 2.73
sys 0.82
LeanPool/LongTails/Proofs/GeneralizedConvergence.lean
import took 1.14s
cumulative profiling times:
attribute application 0.0581ms
congr simp thm 3.76ms
dsimp 3.46ms
elaboration 81ms
fix level params 2.47ms
import 1.14s
initialization 30.8ms
instantiate metavars 3.71ms
interpretation 1.05s
let-to-have transformation 0.795ms
linting 30.1ms
module linting 0.0014ms
norm_num 602ms
overlappingInstancesLinter 6.62ms
parsing 17.9ms
process pre-definitions 15.3ms
ring 86.4ms
share common exprs 23.3ms
simp 34.9ms
tactic execution 301ms
tacticAnalysis 47.3ms
type checking 109ms
typeclass inference 711ms
real 3.59
user 4.02
sys 1.02
LeanPool/LongTails/Proofs/GeneralizedGradientStep.lean
import took 1.13s
cumulative profiling times:
attribute application 0.105ms
blocked (unaccounted) 0.0517ms
congr simp thm 5.05ms
dsimp 0.867ms
elaboration 67ms
fix level params 2.38ms
import 1.13s
initialization 39.7ms
instantiate metavars 1.77ms
interpretation 703ms
let-to-have transformation 4.82ms
linting 20.1ms
module linting 0.00163ms
norm_num 64.5ms
overlappingInstancesLinter 6.89ms
parsing 12.3ms
process pre-definitions 9.93ms
ring 41.1ms
share common exprs 15ms
simp 138ms
tactic execution 264ms
tacticAnalysis 36.8ms
type checking 104ms
typeclass inference 1.19s
real 2.90
user 3.57
sys 1.01
LeanPool/LongTails/Proofs/GeneralizedLogCharging.lean
import took 1.15s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 111ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 411ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 439ms
cumulative profiling times:
attribute application 0.074ms
congr simp thm 3.44ms
dsimp 4.38ms
elaboration 63.4ms
fix level params 3.18ms
import 1.15s
initialization 30.7ms
instantiate metavars 6.92ms
interpretation 2.15s
let-to-have transformation 1.6ms
linting 46ms
module linting 0.00194ms
norm_num 308ms
overlappingInstancesLinter 4.43ms
parsing 24.8ms
process pre-definitions 21.8ms
ring 132ms
share common exprs 35.6ms
simp 66.5ms
tactic execution 434ms
tacticAnalysis 63.5ms
type checking 126ms
typeclass inference 947ms
real 4.07
user 5.31
sys 1.01
LeanPool/LongTails/Proofs/GeneralizedMixedRate.lean
import took 1.15s
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 138ms
cumulative profiling times:
attribute application 0.198ms
congr simp thm 5.49ms
dsimp 13.7ms
elaboration 209ms
fix level params 5.7ms
import 1.15s
initialization 40ms
instantiate metavars 8.47ms
interpretation 1.92s
let-to-have transformation 7.06ms
linting 107ms
module linting 0.0018ms
norm_num 373ms
overlappingInstancesLinter 14.6ms
parsing 46.5ms
process pre-definitions 38.8ms
ring 162ms
share common exprs 56ms
simp 122ms
tactic execution 668ms
tacticAnalysis 150ms
type checking 251ms
typeclass inference 1.52s
real 3.70
user 6.55
sys 1.05
LeanPool/LongTails/Proofs/GeneralizedSelfNormalizedConvergence.lean
import took 1.15s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 188ms
cumulative profiling times:
attribute application 0.0508ms
congr simp thm 3.59ms
dsimp 3.44ms
elaboration 90ms
fix level params 2.37ms
import 1.15s
initialization 30.4ms
instantiate metavars 3.64ms
interpretation 1.17s
let-to-have transformation 0.286ms
linting 25.7ms
module linting 0.00151ms
norm_num 586ms
overlappingInstancesLinter 5.29ms
parsing 17.4ms
process pre-definitions 14ms
ring 93.7ms
share common exprs 22.3ms
simp 25.5ms
tactic execution 261ms
tacticAnalysis 39.4ms
type checking 85ms
typeclass inference 801ms
real 3.35
user 4.16
sys 1.00
LeanPool/LongTails/Setups/GeneralizedSmoothAndConvex.lean
import took 1.11s
cumulative profiling times:
attribute application 0.628ms
blocked (unaccounted) 1.28ms
compilation (IR) 0.0446ms
compilation (LCNF base) 0.309ms
compilation (LCNF impure) 0.233ms
compilation (LCNF mono) 0.396ms
congr simp thm 0.947ms
elaboration 38.3ms
fix level params 0.0816ms
import 1.11s
initialization 32.8ms
instantiate metavars 0.0927ms
interpretation 226ms
let-to-have transformation 0.0371ms
linting 4.3ms
module linting 0.00143ms
overlappingInstancesLinter 0.999ms
parsing 3.39ms
process pre-definitions 1.91ms
share common exprs 0.195ms
simp 0.437ms
tacticAnalysis 9.95ms
type checking 9.52ms
typeclass inference 72.1ms
real 2.17
user 1.28
sys 0.97
LeanPool/LongTails/Setups/SmoothAndConvex.lean
import took 1.12s
cumulative profiling times:
attribute application 0.627ms
blocked (unaccounted) 1.35ms
compilation (IR) 0.0458ms
compilation (LCNF base) 0.313ms
compilation (LCNF impure) 0.237ms
compilation (LCNF mono) 0.435ms
congr simp thm 0.479ms
elaboration 31.2ms
fix level params 0.0589ms
import 1.12s
initialization 30ms
instantiate metavars 0.0763ms
interpretation 228ms
let-to-have transformation 0.0344ms
linting 3.86ms
module linting 0.00151ms
overlappingInstancesLinter 1.26ms
parsing 2.77ms
process pre-definitions 1.56ms
share common exprs 0.136ms
simp 0.406ms
tacticAnalysis 7.7ms
type checking 8.3ms
typeclass inference 58.7ms
real 2.16
user 1.27
sys 0.98
LeanPool/LongTails/Template.lean
import took 1.11s
cumulative profiling times:
attribute application 0.486ms
blocked (unaccounted) 32.1ms
compilation (IR) 1.08ms
compilation (LCNF base) 9.5ms
compilation (LCNF impure) 4.73ms
compilation (LCNF mono) 10.3ms
congr simp thm 0.396ms
elaboration 72.1ms
fix level params 0.115ms
import 1.11s
initialization 30.5ms
instantiate metavars 0.18ms
interpretation 249ms
let-to-have transformation 1.71ms
linting 8.59ms
module linting 0.00142ms
overlappingInstancesLinter 1.71ms
parsing 7.07ms
process pre-definitions 6.67ms
share common exprs 0.356ms
simp 0.952ms
tacticAnalysis 13.1ms
type checking 28.5ms
typeclass inference 26.8ms
real 2.17
user 1.37
sys 0.96
LeanPool/LongTails/Theorems/GeneralizedSelfNormalizedConvex.lean
import took 1.15s
cumulative profiling times:
attribute application 0.0171ms
congr simp thm 0.747ms
elaboration 19.5ms
fix level params 0.764ms
import 1.15s
initialization 35.7ms
instantiate metavars 0.853ms
interpretation 238ms
let-to-have transformation 0.105ms
linting 4.39ms
module linting 0.00142ms
overlappingInstancesLinter 1.54ms
parsing 3.59ms
process pre-definitions 3.23ms
share common exprs 1.36ms
simp 4.1ms
tactic execution 61.7ms
tacticAnalysis 16.1ms
type checking 10.9ms
typeclass inference 61.2ms
real 2.27
user 1.36
sys 0.98
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Collaborator
Author
|
/review Exact head: |
Collaborator
Author
|
Updated thorough source review — APPROVE at {
"review": "Acquisition source review, separate pass over the final import",
"head_sha": "b76327d4558dc868a546f55ee79820991b4898c6",
"conclusion": "approve",
"reviewer_scope": "A separate review pass by the acquisition agent; the configured GPT review remains the independent verdict.",
"coverage": {
"upstream": "All 17 modules in the selected dependency closure, 2,605 upstream lines, inspected in bounded chunks; all endpoint declarations and transitive imports covered.",
"diff": "All 20 added files at this head, including the 19 Lean modules/wrappers and project YAML; all source edits beyond the mechanical port reviewed. Follow-up review covers the complete four-file extraction of proved charging and energy-to-weight facts.",
"build_and_profiles": "Warning-free clean build, generated indexes, style, static quality, 518-declaration lint/trust checks, clean timing logs and command-heartbeat profiles inspected.",
"ci": "Required and advisory checks are rerunning on this new head; no pending result is treated as success."
},
"merge_eligibility": "Wait for required CI and configured independent reviews, resolve every material finding, then use normal protected queue validation. This source approval does not waive any gate or the infrastructure priority hold.",
"faithfulness": {
"verdict": "pass",
"bottom_line": "The card describes the actual generalized-smooth convex objective-gap and exact gradient-query guarantee.",
"proves_the_claim": "proves_it",
"claim_note": "SelfNormalized.result supplies one algorithm family from Public information, uniformly over positive target accuracy, with the stated ceiling/minimum budget; execute_gradient_oracle equates 2*N queries with N genuine accelerated steps.",
"assumed_inputs": "A complete real inner-product space; convexity; an everywhere differentiable exact gradient satisfying the Hessian-growth norm bound; an attained minimum; positive L0, R, Delta and epsilon, and nonnegative L1. These are disclosed in the card. Oracle correctness is required at every call and sample; no convergence claim is hidden in a structure field.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "The examined libraries do not contain the selected discrete generalized-smooth, gradient-only oracle-complexity endpoint.",
"already_formalized": "",
"novelty_note": "Mathlib gradient calculus and Tau Ceti norm_gradient_eq_norm_fderiv, maximal-slope-flow convergence and Moreau-Yosida existence statements do not provide this finite-query algorithm. The pool's ParameterFreeGradient project targets gradient-norm accuracy under global Lipschitz smoothness in finite-dimensional lp spaces, with a different oracle/model. Searches were bounded; this is a negative search finding, not an exhaustive equivalence proof.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a completed research-level convergence development with reusable mathematical and oracle-execution infrastructure.",
"fit": "good_fit",
"level": "research",
"branch": "convex optimization",
"mode": "theory_building",
"significance_one_sentence": "The formalization preserves a gradient-only accelerated bound under gradient-dependent Hessian growth, with explicit accounting, local gradient estimates, energy dissipation, charging and weighted inequalities.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The exact upstream formalization, license, completion commit and credited authors support the import's stated scope.",
"source_match": "matches",
"findings": []
},
"code_quality": {
"verdict": "pass",
"bottom_line": "Both convergence arguments reuse proved charging geometry and energy-to-weight facts; targeted imports and explicit linear arithmetic avoid duplicated elaboration and unnecessary search.",
"code_quality": 3,
"findings": []
},
"engineering_checks": {
"algorithm_and_boundary_cases": "Checked the Delta<=epsilon zero-query return, L1=0 branch, positivity requirements, natural ceiling, both queries per step, and the choice of the smaller of two bounds for the same algorithm. Exact-gradient uniqueness makes execution independent of the oracle seeds; it does not assume an optimizer oracle or free function-value evaluations.",
"nonvacuity": "The assumptions admit ordinary smooth convex quadratics; no constructor or bundled predicate asserts descent, termination accuracy or the main convergence bound.",
"trust": "The existing axiom and compiled-declaration audits pass over all owned modules, including auxiliary/generated declarations, with only Classical.choice/propext/Quot.sound permitted. No prohibited mechanism, heartbeat override, suppression or gate edit is introduced.",
"attribution_and_scope": "Apache-2.0 source, upstream authors and AI proof provenance recorded. Only the selected mathematical closure is imported; unrelated upstream automation and third-party UI assets are absent. LeanPool.lean remains byte-identical.",
"compile": "Comparable clean builds: 47.81s -> 36.28s; max RSS 1,784,552 -> 1,528,748 KiB. Main accuracy proof command profile: 122,991 -> 18,197 heartbeats. Shared facts now also eliminate the duplicate derivations identified by Greptile; both bounds and all headline statements are preserved."
},
"previous_review": "https://github.com/LeanPool/lean-pool/pull/693#issuecomment-6288059552",
"review_response": {
"greptile_comment": "https://github.com/LeanPool/lean-pool/pull/693#discussion_r4323600614",
"repair": "run_charging_geometry proves the shared low/high-curvature, prefix, injectivity and count facts; run_weight_le_of_inaccurate derives the weight bound from a failed accuracy target. Both results consume these helpers."
}
} |
Collaborator
Author
|
/review |
Collaborator
Author
|
/review Exact head: |
Collaborator
Author
|
Thorough review addendum for the current card-only head: {
"head_sha": "f4a2221c18f1ea33bb97e2d5dbdfb8590dbc62fa",
"conclusion": "approve",
"prior_full_review": "https://github.com/LeanPool/lean-pool/pull/693#issuecomment-6288257852",
"reviewed_delta": "Only the ordinary gradient-descent informal result changed: L>0, R>=0 and epsilon>0 are now explicit and match gd_accuracy.",
"validation": "Existing card, metadata and declaration checks pass. All Lean sources and project inputs are byte-identical to the prior reviewed head; the 518-declaration build/lint/trust results and 36.28s clean measurement remain applicable.",
"merge_eligibility": "Await current-head required CI and the independent GPT verdict; all protected queue requirements remain in force."
} |
Vilin97
commented
Oct 20, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
Author
There was a problem hiding this comment.
Independent Source review — APPROVE at f4a2221c18f1ea33bb97e2d5dbdfb8590dbc62fa.
{
"review": "Permanent reviewer — independent Source review",
"head_sha": "f4a2221c18f1ea33bb97e2d5dbdfb8590dbc62fa",
"conclusion": "approve",
"coverage": "All 20 added files: the full 17-module mathematical closure, public entry, generated Imports, and project card. The four-file helper extraction and final card-only correction were reviewed against complete before/after source; unchanged intervals were verified byte-identical.",
"faithfulness": {
"verdict": "pass",
"proves_the_claim": "proves_it",
"bottom_line": "The disclosed objective-gap and exact-gradient-query guarantee matches SelfNormalized.result.",
"claim_note": "Convergence selects one algorithm from Public before quantifying target accuracy, hidden objective and oracle. The admissibility predicate explicitly requires convexity, exact gradients at every sample/call, a differentiable gradient field, the Hessian-growth bound, and an attained minimizer with the initial radius and objective-gap bounds. It assumes no descent or convergence conclusion. execute_gradient_oracle accounts for both queries, including initialization; Delta <= epsilon returns x0 with zero queries. The L1 = 0 case is retained, and run_accuracy_min combines two proved bounds on the same algorithm/run.",
"assumed_inputs": "Real complete inner-product space; positive L0, R, Delta and epsilon; nonnegative L1. The final card also explicitly discloses L > 0, R >= 0 and epsilon > 0 for the ordinary gradient-descent auxiliary.",
"findings": []
},
"novelty": {
"verdict": "pass",
"already_formalized": "",
"bottom_line": "The inspected nearest library contracts are distinct from this finite-query generalized-smooth convergence theorem.",
"novelty_note": "Compared actual Mathlib gradient/convexity declarations, TauCeti's norm_gradient_eq_norm_fderiv, maximal-slope limit and Moreau-Yosida existence results, and the pool's V7.MainStatement for ParameterFreeGradient. The latter targets finite-dimensional dual-lp gradient-norm accuracy with pair-oracle accounting. These do not supply this Hilbert-space objective-gap theorem. This is a bounded contract comparison, not an exhaustive global absence or priority claim.",
"findings": []
},
"significance": {
"verdict": "pass",
"fit": "good_fit",
"level": "research",
"branch": "convex optimization",
"mode": "theory_building",
"bottom_line": "A completed research-level development with substantial reusable proofs.",
"significance_one_sentence": "The explicit gradient-only guarantee is supported by oracle execution, local gradient growth estimates, damped energy dissipation, charging geometry and two complementary quantitative convergence arguments.",
"findings": []
},
"sources": {
"verdict": "pass",
"source_match": "matches",
"bottom_line": "The pinned upstream development, attribution and declared proof provenance support the import.",
"source_note": "Verified Apache-2.0 at upstream 269cbc764dd36851fd0b64f2f950f329ee127de4 and all 17 selected producer blobs against completion commit 32aa9399511f9a11ecffb74ca284d8229bfd80c0 (2026-10-14). The four named authors and AI provenance are supported by the upstream public metadata. Source-to-port inspection preserves the analytic model, algorithm and exact budget. Related paper bounds provide context; they are not claimed as exact sources for the imported 4096/min formula.",
"findings": []
},
"code_quality": {
"verdict": "pass",
"code_quality": 3,
"bottom_line": "Competent structure with the concrete duplication issue addressed.",
"quality_note": "run_charging_geometry proves the shared charging facts once; run_weight_le_of_inaccurate derives the failed-accuracy weight bound from the actual energy inequality. Both distinct convergence results and all existing statement headers remain. The new helpers add no assumed correctness fields. The import preserves unrelated projects, LeanPool.lean, dependency pins and all gates.",
"findings": []
},
"resolved_findings": [
{
"path": "LeanPool/projects/longtails-generalized-convex.yaml",
"issue": "The ordinary GD prose omitted the theorem's positive smoothness/accuracy and nonnegative radius regime.",
"resolution": "Fixed in f4a2221: only this informal card field changed; all Lean statements and proofs are unchanged by the correction."
},
{
"thread": 4323600614,
"issue": "Repeated charging and failed-accuracy arguments.",
"resolution": "The reviewed b76327d helper extraction addresses this advice; f4a2221 retains those exact Lean bodies. The existing thread is resolved."
}
],
"validation": "This is Source acceptance at the exact head. The current configured review and full applicable authored/native CI still have to qualify before protected queue admission. Author build, declaration-audit and timing claims remain attributed; no pending job, old-head result or advisory profile is treated as current CI success."
}
Collaborator
Author
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All four card claims match the Lean, including boundary cases and query accounting; CI remains pending, and no local rebuild was performed. |
| Novelty | ✅ pass |
No duplicate of the four headlines was identified in the checked Mathlib, Tau Ceti, or pooled declarations. |
| Significance | ✅ pass |
The accelerated oracle-complexity theorem and its supporting analysis meet the research-level significance bar. |
| Sources | ✅ pass |
The pinned upstream formalization supports the stated result, hypotheses and query budget, and is explicitly credited throughout the import. |
| Code quality (advisory) | ✅ pass |
The proofs are competently factored around shared charging and energy helpers, with no material maintenance findings; current-head CI remains pending. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The card discloses the complete real Hilbert space, convexity, differentiable exact gradient, Hessian-growth bound, attained minimizer, initial distance and objective-gap bounds, positive L0, R, Delta and epsilon, and nonnegative L1. Oracle correctness holds at every call and seed. The ordinary gradient-descent result assumes a globally L-Lipschitz exact gradient and distance to a comparison point; it does not require that point to minimize the objective. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | convex optimization |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: SelfNormalized.result supplies an algorithm family independent of target accuracy and the hidden objective, achieving the stated objective-gap guarantee with the exact ceiling/minimum budget, including zero queries when the initial-gap bound meets the target.
SelfNormalized.result establishes an explicit gradient-query bound for generalized-smooth convex optimization on real Hilbert spaces, supported by local gradient estimates, energy dissipation, charging arguments, and two complementary convergence bounds.
Tokens: 6,929,227 in / 34,113 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $28.2286 (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
|
Final validation checkpoint — APPROVE at Current-head Lean Action CI has succeeded: full-pool warning-free build, declaration lint, style, and repository quality/trust audits all passed. The configured five-rubric GPT review approves this exact head. Greptile is successful, its shared-proof finding was repaired, and every review thread is resolved. The thorough source review and independent Source review remain applicable without any source change. No material finding remains. Main is still |
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.
This imports a completed LongTails result on gradient-only acceleration for convex objectives with generalized smoothness: the Hessian bound is
‖D∇f(x)‖ ≤ L0 + L1‖∇f(x)‖. The theorem gives an explicit query budget with the improved(L1 R)^(2/3)dependence, retaining its logarithmic factors, initial objective-gap bound, attained minimizer, and Hilbert-space hypotheses. It counts both gradient queries in every accelerated step and uses no objective-value or line-search oracle.The headline is
LongTails.OracleTemplate.GeneralizedAccelerated.SelfNormalized.result. The card gives the complete ceiling/minimum formula rather than claiming an optimal rate. The zero-queryDelta ≤ epsiloncase andL1 = 0case are preserved.Source and eligibility
AI, reflecting the upstream agent-generated proof workflow.GeneralizedSelfNormalizedConvex. It preserves reusable oracle execution, ordinary gradient descent, local gradient/Hessian estimates, energy dissipation, block charging, weighted inequalities and both convergence bounds. Other LongTails results, automation, UI, fonts and external tooling are outside this import.Port and engineering
Ported to the pool's exact Lean
v4.35.0-rc3and Mathlibc55e6e786f49471c72fbddbec5415808896aec1e. Modules use explicit public visibility, implementation declarations are isolated underLongTails.OracleTemplate, and the execution loop is public so module-system clients can unfold execution. Added API/field documentation and removed unnecessary decidable-equality parameters. Mathematical hypotheses, the algorithm, theorem strength, query count and budget formulas are preserved.One YAML card and its generated public
Imports.leanare added.LeanPool.leanis unchanged. No gate, configuration, waiver or dependency pin changes are included.Measured compile optimization
Command:
lake build LeanPool.LongTails.Imports, after deleting only this project's build artifacts. Both runs used warm pinned dependency caches, default Lake parallelism, and the same shared Azure VM (16 available CPUs, AMD EPYC 9V45); ordinary shared-host timing variation remains.run_accuracy_self_normalizedcommand heartbeatsRemoved five broad
Mathlib.Tacticimports in favor of the needed theory/tactic modules. Profile-guided repairs replace unrestricted nonlinear searches with explicit linear combinations of the required energy/count inequalities. In response to Greptile, both convergence arguments now reuse proved charging geometry and energy-to-weight helpers, preserving both bounds. Wall time improves about 24%, and the profiled declaration drops about 85%. Heartbeat figures use synchronous command profiling; nested theorem/lemma macro traces are counted once per declaration. No heartbeat/recursion overrides are present. Remaining proof modules and reusable generality are retained.Validation
lake exe mk_all --module --check: pass.lake exe lint-style LeanPool.LongTails.Imports: pass.git diff --checkand content-only scope check: pass. No Python implementation changed.CI remains the final authority. Configured GPT and Greptile reviews and a separate thorough source review will be recorded on this PR before any protected queue entry. Daily documentation publishing is asynchronous under PR659 and is assessed separately from required validation.