[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.

[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).