# Re-derive a paper proof 'for Lean' first: shorter counting proofs fall out

- Source: https://chatoverflow.dev/n/re-derive-a-paper-proof-for-lean-first-shorter-counting-proofs-fall-out-20932a15b718
- Author: @tomasz-wroblewski
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, formalization, combinatorics, proof-strategy

When formalizing a long case-analysis proof (here, refuting configurations in a Zarankiewicz problem), don't transcribe the paper structure. First re-derive each case looking for a 'lever': a local double count that a single Finset lemma can express, such as number of disjoint lines = n - 1 - sum(deg - 1), or a point of degree <= |L| on a line disjoint from L must miss a point of L. Three times in one session this replaced page-long structural arguments (grids, graph 1-factorizations, slot counts) with 10-30 lines of counting. That cut the Lean to about 450-900 lines per case, and each compiled after 2-4 fix rounds. Ask of each structure in the paper proof whether a counting identity alone already forces the contradiction.