[loefflerd]

Summary

The 200-line proof-size check currently treats everything up to the next theorem or lemma as part of the preceding proof. Consequently, a two-line proof followed by definitions or instances can be reported as hundreds of lines long. It also mistakes assignments in theorem statements for the start of the proof.

This change replaces the existing Python-based parser with a Lean linter, enforcing the same 200-line maximum but using Lean's own syntax trees to reliably count lines.

No mathematical content or project metadata is changed.

See #723 for an issue tracking over-long proofs in extant LeanPool code which were overlooked due to bugs in the existing checker.

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[greptile-apps]

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 confirmed issue blocks merging this PR.

Summary

Replaces the Python proof-length scan with a Lean compiler plugin that checks proof syntax and elaborated types.

• Lean measures each proof against the 200-line limit.

Review used the full PR changes because the previous and current review commits have different merge bases with the target commit. No tests were executed.

_{Reviews (7) · Last reviewed commit: "Merge main into CI-theorem-lines" · Reviewed by Greptile}

[loefflerd]

Aargh. It looks like this proposed Python script change just exchanges the quirks and corner cases of the existing script for a different set. Probably the only tool that can reliably parse Lean code is Lean itself; I'll look into writing a Lean proof-length linter (analogous to the existing line-length linter).

[Vilin97]

Reviewed all nine changed files and all 15 hunks at 4cf748e, including the complete plugin and compiler fixtures. Original source ranges, semantic proof classification, comment handling, overlapping ranges and the production 200/201 boundary have coherent coverage. I found no isolated-head correctness defect from this static review.

The policy decision is broader than replacing the parser: blank lines now count, and proof terms inside definitions, instances and examples become subject to the cap. Moving enforcement into the compiler/warning gate also changes protected tooling, workflow and cache inputs. These changes need direct scoped authorization under the repository rules; the default cap remaining 200 does not by itself preserve the old policy.

There is a small integration fix when composing this with #719: test_proof_length_plugin_has_pinned_ci_coverage requires the exact substring -k 'test_lake_', while #719 extends it to -k 'test_lake_ or test_compiled_axiom_audit'. Check the selector semantically and retain both fixture suites. This is a combined-tree issue, not a claimed failure of this head. Compiler fixtures and current CI were not independently run here.

[Vilin97]

Integration status at 4cf748ef8998b66e6ec6368aacc7eb5189cdda10: the favorable implementation review is retained. It does not resolve the existing-content repairs tracked in #723. Please address those over-limit proof terms in separate proof-preserving content changes: factor the reported AndersonConjecture PLift proofs and PLAcceleratedNesterovLean private abbrev proofs into meaningful intermediate lemmas, preserving the mathematical contracts. Keep #723 open until the repaired source passes the semantic checker and normal validation; changing declaration spelling or adding a waiver is not a repair. I have not reproduced fresh compiler counts for those project files.

The current direct gate-change authorization covers #719 only. This PR still needs its own scoped authorization. It follows #719; when composing them, retain both fixture suites and update this PR’s exact-selector assertion. These are separate integration conditions, with the nine-file source review already complete.

[Vilin97]

Thanks for this — the syntax-aware checker is a clear improvement, and it found real loopholes. To get it merged:

• The 22 over-long proofs it flags (tracked in Long proofs exploiting loopholes in proof-length checker #723) are split in Split over-long proofs in AndersonConjecture #756 (AndersonConjecture) and Split over-long proofs in PLAcceleratedNesterovLean #757 (PLAcceleratedNesterovLean). A full-pool run of this linter on current main found no other violations.
• I merged current main into this branch (ff2d4fc), composing with fix axiom-audit checker to use Lean env rather than source parsing #719: the three pinned-Lean pytest steps now run both compiled-fixture suites with fix axiom-audit checker to use Lean env rather than source parsing #719's selector, and test_proof_length_plugin_has_pinned_ci_coverage checks that the selector includes test_lake_ instead of matching it exactly.

Once #756 and #757 are in, CI here should be green and this will go into the merge queue.

🤖 Generated with Claude Code

[Vilin97]

{
"summary": "Reviewed current ff2d4fc and all nine changed files against current main and the previously reviewed implementation. The proof-length plugin and Lean fixtures are unchanged; the three pinned-Lean pytest steps retain both fixture suites, and the selector test now parses argv and checks test_lake_ membership. The existing axiom auditor is preserved. The current worker assignment supplies the direct scoped gate-change authorization. Source review is favorable; PR756 and PR757 must land first, and this head must then pass its own applicable protected checks before queue admission.",
"assessment": {
"scope": "Syntax-aware proof-length enforcement and PR719 fixture composition",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The selector composition is fixed without changing the already validated plugin semantics or weakening the existing audit."
},
"verdict": "approve",
"findings": []
}

[loefflerd]

See also leanprover-community/mathlib4#45388, a Mathlib PR contributing a descendant of the long-proofs linter from this PR to Mathlib's standard linter set (which will eventually render this LeanPool PR redundant).

[Vilin97]

Reviewed published head 2a50c58ef221eb6dc2e8c8a1d161e9d1fa7cd2e1.

All nine changed source files are byte-identical to the previously reviewed ff2d4fc59 implementation. I checked the published two-parent merge against current main 6814773, including the complete forward/inverse tree reconstruction. The proof-length plugin, regression fixtures, all three pinned-Lean selectors, and the existing axiom auditor retain the reviewed composition; unrelated projects and controls are preserved.

PR756 and PR757 have now both merged. The direct scoped authorization for this PR is resolved, and my source verdict remains favorable at this exact new head. The current-head CI run and applicable current-main validation still need to complete before normal protected queue admission. Earlier-head CI and the targeted compiler checkpoint have not been credited to this revision.