[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] The PR appears safe to merge; the previous finding is fixed and no new actionable issues were found.

Summary

Replaces the Python proof-length scan with a Lean compiler plugin.

• Lean counts proof lines from each proof's actual source span.

_{Reviews (5) · Last reviewed commit: "avoid long functions in long proof test" · 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.