Repository navigation
Split over-long proofs in PLAcceleratedNesterovLean - #757
Conversation
Refactor every proof over 200 lines (as measured by the syntax-aware long-proof linter in #712) into named helper lemmas. Proof carriers disguised as PLift-valued defs or private abbrevs become theorems. Statements and public declarations are unchanged. Refs #723 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low impact] No actionable regression was found in the reviewed proof refactor. SummarySplits long proofs into named helpers and shares the contraction and bootstrap arguments.
Reviews (2) · Last reviewed commit: "Extract fderiv_kills_normal_of_eqOn from..." · Reviewed by Greptile |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "The seven-file refactor decomposes the eight long Nesterov proofs into named mathematical steps and shares the bootstrap induction and state-level contraction argument while preserving existing public contracts. This is a source verdict; current normal CI and execution of the intended semantic checker remain pending.",
"assessment": {
"scope": "Proof decomposition and reuse in the existing PLAcceleratedNesterovLean project.",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Named geometry, displacement and contraction lemmas replace long duplicated proof bodies without changing the existing public hypotheses or conclusions."
},
"verdict": "approve",
"findings": []
}
Proof profile (new / modified Lean files)Statement changes
|
| File | Δ lines | HB base | HB head | Δ HB | Δ HB % | Wall base (s) | Wall head (s) |
|---|---|---|---|---|---|---|---|
LeanPool/PLAcceleratedNesterovLean/Convergence/Bootstrap/Main.lean |
+165/-425 | 310,382 | 127,387 | -182,994 | -59.0% | 60.78 | 25.33 |
LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/Derivative.lean |
+253/-229 | 286,734 | 247,262 | -39,472 | -13.8% | 44.76 | 17.26 |
LeanPool/PLAcceleratedNesterovLean/Convergence/GenLocalArgument.lean |
+312/-263 | 92,897 | 74,794 | -18,103 | -19.5% | 24.03 | 13.12 |
LeanPool/PLAcceleratedNesterovLean/Core/EmbeddedManifold.lean |
+194/-158 | 586,229 | 576,119 | -10,110 | -1.7% | 88.23 | 41.52 |
| Total | +924/-1,075 | 1,276,241 | 1,025,562 | -250,680 | -19.6% | 217.8 | 97.2 |
New files — absolute profile
Total heartbeats: 330,323 maxHeartbeats units across 2 valid files (930 added LOC).
Sum of lean --profile: — across 0 valid files. Import-excluded time: —.
Count-heartbeats wall-clock total: 46.60 s. Repeated import cost inside lean --profile: —.
Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.
LOC counts added lines in the profiled Lean files from this PR diff.
| File | LOC | Heartbeats (maxHB) | Count wall (s) | lean --profile (s) |
Without import (s) | Import (s) | Commands | Errors |
|---|---|---|---|---|---|---|---|---|
LeanPool/PLAcceleratedNesterovLean/Convergence/LocalGeometry/Main.lean |
494 | 172,377 | 31.10 | — | — | — | 23 | 0 |
LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/GenMain.lean |
429 | 157,946 | 15.50 | — | — | — | 15 | 0 |
LeanPool/PLAcceleratedNesterovLean/Convergence/LyapunovContraction/Main.lean |
7 | — | — | — | — | — | 9 | 1 |
| Total | 930 | 330,323 | 46.60 | — | — | — | 47 | 1 |
Aggregate phase totals
| Phase | Time |
|---|---|
| Unavailable | — |
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Main's text-based proof-size check counted the statement's let-bindings as proof and reached 201 lines; extracting this self-contained step brings it comfortably under the limit for both checkers. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "The current follow-up extracts the private derivative-equality step without changing any existing contract. The seven-file refactor preserves public hypotheses and conclusions while sharing bootstrap and contraction arguments and decomposing the eight long proofs. Current-head normal CI and execution of the intended semantic checker remain pending.",
"assessment": {
"scope": "proof decomposition and shared mathematical arguments",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "low",
"assessment_one_sentence": "The current exact-head continuation preserves the accepted mathematical contracts and proof structure."
},
"verdict": "approve",
"findings": []
}
|
/review Please review the current published head 3ce4c27. The independent source continuation is posted; older-head reviews and checks remain dated. |
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | proof extraction and deduplication |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ➖ unchanged |
| Risk | ✅ low |
The shared proofs and named helpers reduce maintenance duplication while preserving the mathematical structure and existing tactic discipline.
Tokens: 3,676,482 in / 6,657 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $14.8058 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
CI was not green for this commit at review time; this review does not replace CI.
|
Targeted validation at exact head 3ce4c27 passed with Lean 4.35.0, the pinned Mathlib revision, the unchanged proof-length plugin from #712, the normal project options and warningAsError. The 40-module dependency closure includes all seven modified modules: 38 project modules compiled quietly, with two unchanged modules reused from verified prior passes; 15 missing Mathlib dependency modules were also compiled. The intended semantic proof-length checker emitted no warning. The separate 200/201 boundary controls and original over-limit baseline were preserved, not rerun. This covers the modified files and their dependency closure. Full-project build/lint/style/quality, required contexts and native integration checks remain separate; this is not a compile-cost comparison or a closure of #723. |
Brings in the long-proof splits from LeanPool#756 and LeanPool#757 so the new linter passes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Prerequisite for #712 (syntax-aware proof-length linter). That linter correctly finds 8 proofs in PLAcceleratedNesterovLean over the 200-line cap; the old text-based checker missed them because they were carried by
private abbrevs.localFiberwiseGeometryProof, 663 → 79 lines; every proof now ≤ 176).lyapunov_contraction_of_state; the two public theorems are short wrappers. Likewise the two bootstrap displacement proofs share one induction lemma.private abbrevs becomeprivate theorems. Unused intermediate facts and redundant imports were dropped.set_option,sorry,native_decideor nolints.Verified locally against current main with #712's linter enabled:
lake build LeanPool.PLAcceleratedNesterovLean.Importsemits zero warnings;scripts/ci/lint-project.leanpasses on all 63 modules (721 declarations);lake exe lint-style LeanPoolpasses.Refs #723
🤖 Generated with Claude Code