Long proofs exploiting loopholes in proof-length checker #723

In PR #712 I implemented a new proof-length checker using Lean's syntax trees rather than the existing ad-hoc Python source parsing. This fails CI because it correctly identifies several very long proofs in existing LeanPool code, which are missed by the existing proof-length checker:

• Several files in AndersonConjecture, e.g. LeanPool/AndersonConjecture/Jensen/KrullDomain/KrullDomain.lean: use PLift to disguise propositions as data
• Two files in PLAcceleratedNesterov, e.g. LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/Derivative.lean: long proofs declared as private abbrev

These seem to be the only examples in LeanPool at present; see CI run https://github.com/LeanPool/lean-pool/actions/runs/40647364991?pr=712