Repository navigation
Split over-long proofs in AndersonConjecture - #756
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] The latest changes introduce no blocking issue; they only separate declaration prefixes from the declarations. SummarySplits long proofs in
Reviews (4) · Last reviewed commit: "Put theorem headers on their own line af..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Proof profile (new / modified Lean files)Statement changes
|
| File | Δ lines | HB base | HB head | Δ HB | Δ HB % | Wall base (s) | Wall head (s) |
|---|---|---|---|---|---|---|---|
LeanPool/AndersonConjecture/Jensen/KrullDomain/KrullDomain.lean |
+183/-448 | 381,531 | 269,716 | -111,815 | -29.3% | 33.48 | 17.31 |
LeanPool/AndersonConjecture/Jensen/KrullDomain/UFDConstruction.lean |
+218/-262 | 297,898 | 398,473 | +100,575 | +33.8% | 28.70 | 13.92 |
LeanPool/AndersonConjecture/Jensen/CloseUp/AvoidanceStep.lean |
+422/-404 | 66,957 | 137,693 | +70,735 | +105.6% | 17.20 | 10.31 |
LeanPool/AndersonConjecture/Jensen/Construction/Transfinite.lean |
+289/-305 | 88,102 | 143,441 | +55,339 | +62.8% | 17.78 | 9.17 |
LeanPool/AndersonConjecture/Jensen/CombinedStep.lean |
+124/-96 | 166,411 | 199,896 | +33,485 | +20.1% | 24.22 | 11.30 |
LeanPool/AndersonConjecture/Jensen/KrullDomain/HeightBound.lean |
+338/-402 | 284,986 | 307,230 | +22,244 | +7.8% | 32.12 | 17.21 |
LeanPool/AndersonConjecture/Jensen/CloseUp/NoCommonFactor.lean |
+438/-446 | 115,518 | 136,770 | +21,252 | +18.4% | 16.74 | 12.00 |
LeanPool/AndersonConjecture/Jensen/CloseUp/Factor.lean |
+204/-221 | 47,270 | 45,375 | -1,896 | -4.0% | 12.56 | 8.17 |
LeanPool/AndersonConjecture/Jensen/Adjoin/FromPrime.lean |
+224/-203 | 49,396 | 50,405 | +1,009 | +2.0% | 12.36 | 8.72 |
LeanPool/AndersonConjecture/Jensen/CloseUp/CoprimeSplit.lean |
+204/-197 | 58,178 | 59,182 | +1,004 | +1.7% | 15.38 | 6.89 |
LeanPool/AndersonConjecture/AdicNoetherian.lean |
+259/-336 | 237,046 | 236,327 | -719 | -0.3% | 29.56 | 18.03 |
LeanPool/AndersonConjecture/Jensen/Adjoin/Adjoin.lean |
+222/-206 | 52,714 | 53,113 | +399 | +0.8% | 15.99 | 11.22 |
| Total | +3,125/-3,526 | 1,846,008 | 2,037,621 | +191,613 | +10.4% | 256.1 | 144.2 |
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Its only callers were replaced by the coefficient-based argument. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Restore the existing exported smul_lift_of_filtration contract and its bounded proof while retaining the long-proof decomposition. The lemma remains available to downstream users even though current internal callers now use coefficient decomposition. Refs #723.
Main's text-based proof-size check only recognizes declarations that start a line, so one-line 'include T in theorem' headers merged neighbouring blocks into apparent 264/364-line proofs. Splitting the header is the standard layout and keeps both checkers accurate. 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 refactor separates the existing adic, avoidance, transfinite, height and UFD arguments into named proved helpers and removes their PLift proof wrappers. The current head restores the exported lifting lemma unchanged, resolving the sole compatibility finding while retaining the clearer proof structure. The restored exported smul_lift_of_filtration lemma keeps downstream compatibility even though internal callers now use the coefficient construction. Current normal CI and execution of the intended semantic checker remain pending.",
"assessment": {
"scope": "proof decomposition with public API compatibility restored",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "unchanged",
"risk": "low",
"assessment_one_sentence": "The proof decomposition improves maintenance and the exact compatibility restoration resolves the only actionable finding."
},
"verdict": "approve",
"findings": []
}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "The current follow-up only separates include/omit prefixes from declarations at 35 sites. All nonwhitespace tokens in the complete 50-module project remain unchanged from the reviewed compatibility restoration, including the exported smul_lift_of_filtration lemma. Current-head normal CI and execution of the intended semantic checker remain pending.",
"assessment": {
"scope": "formatting continuation of proof decomposition with public API compatibility retained",
"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 4b1e37f. The independent source continuation is posted; older-head reviews and checks remain dated. |
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | proof decomposition and PLift wrapper removal |
| Introduces tech debt | ✅ no |
| Maintainability | ✅ improved |
| Brittleness | ➖ unchanged |
| Risk | ✅ low |
The extracted helpers make the arguments easier to navigate and repair without introducing opaque automation or actionable maintenance debt.
Tokens: 10,884,680 in / 17,071 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $43.7948 (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 4b1e37f passed with Lean 4.35.0, pinned Mathlib, the unchanged proof-length plugin from #712, the normal project options and warningAsError. All 29 project modules in the dependency closure of the 12 modified files compiled quietly with the intended semantic proof-length checker. The run also compiled 58 missing Mathlib dependencies. No old project products were substituted, and the restored public lifting lemma is included. The previously verified 200/201 boundary controls and original over-limit baseline were retained without rerunning them. This establishes the targeted current-file checker result. Full-project build/lint/style/quality, required contexts and native integration remain separate. Both #756 and #757 still need their normal protected merges before #712; #723 remains open until that work is integrated. |
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 14 proofs in AndersonConjecture over the 200-line cap; the old text-based checker missed them because they were carried by
private def ... : PLift (...).*_proofdefs are removed: their proofs now live directly in the theorems they backed (or becomeprivate theorems). Dead intermediate facts and duplicated blocks were dropped.set_option,sorry,native_decideor nolints.Verified locally against current main with #712's linter enabled:
lake build LeanPool.AndersonConjecture.Importsemits zero warnings;scripts/ci/lint-project.leanpasses on all 51 modules (888 declarations);lake exe lint-style LeanPoolpasses.Refs #723
🤖 Generated with Claude Code