Long proofs exploiting loopholes in proof-length checker #723

Activity

1. Vilin97 commented on Nov 5, 2026

   

   Vilin97

   on Nov 5, 2026

   Collaborator

   More actions

   Checked the published sources at 94739c353b4c2ceacb577a4eefad3a9210597484. The Nesterov scope extends to eight large proof abbreviations across seven files. The table uses each outer proof assignment, excluding assignments inside statement-level let expressions.

   These are static written non-comment line counts, with blank lines retained; semantic-linter validation remains required.

   File under LeanPool/PLAcceleratedNesterovLean/	Declaration	Proof lines	Written count
   MorseBott/TubularProjection/Derivative.lean	tubularProj_hasFDerivAt_starProjection	109–408	253
   Core/EmbeddedManifold.lean	smooth_embedding_local_graph	136–458	305
   Convergence/Bootstrap/Main.lean	bootstrapTotalDisplacementProof	111–369	220
   Convergence/Bootstrap/Main.lean	bootstrapTotalDisplacementGenProof	443–751	280
   Convergence/GenLocalArgument.lean	localConvergenceAtBasePointGenProof	107–527	393
   Convergence/LocalGeometry/Main.lean	localFiberwiseGeometryProof	129–936	663
   Convergence/LyapunovContraction/Main.lean	lyapunovContractionProof	133–706	434
   Convergence/LyapunovContraction/GenMain.lean	lyapunovContractionGenProof	123–696	434

   In AndersonConjecture/KrullDomain, the main inner Prop proof packaged in PLift spans lines 327–837 (487 written non-comment lines). Its cardinal-bound subproof at 469–765 accounts for 288. The two kernel proofs are only 61 each; their shared coefficient-map, quotient-evaluation and coset-avoidance arguments offer reusable helper boundaries, rather than additional demonstrated over-limit proofs. Extract finite-fiber/countability lemmas and the two modular-cardinality bounds before assembling the avoiding pair and final theorem. Preserve the three public theorem contracts and prove every intermediate fact from the existing hypotheses.

   For the derivative file, I worked out a bounded three-helper split: scalar projection displacement, the epsilon/error estimate, and the chart derivative chain rule. Its complete source proposal preserves all existing headers/imports and has a byte-exact inverse outside those extractions; its written proof count falls from 253 to 187. That proposal is unapplied and uncompiled. The remaining seven Nesterov proofs and the Anderson argument require substantial mathematical decomposition.

   Please land the repairs as separate proof-preserving content changes. Validate each changed module with the unchanged intended semantic checker and normal build/lint/quality checks, then close this issue when the complete affected scope passes. Keep the 200-line limit and mathematical statements intact. PR712’s separate scoped gate authorization and its paired PR719 fixture-selector integration remain independent conditions.
2. Vilin97

   added 4 commits that reference this issue on Nov 5, 2026

   refactor: split tubular projection derivative proof

   ...

   a8c4100

   Preserve the public filtration lifting lemma

   ...

   ad05935

   Split over-long proofs in AndersonConjecture (LeanPool#756)

   ...

   c0b2df7

   Split over-long proofs in PLAcceleratedNesterovLean (LeanPool#757)

   ...

   6814773