We are looking for proofs that are long enough to leave room for shortening, ideally expensive to compile (high heartbeat), and whose statement exists unchanged across several toolchains, so they can be replayed and compared across Lean versions.

1. Long

Ideally well over 30 lines for the whole declaration (statement + proof). Existing records run 55–209 lines. Short proofs leave no slack — there is nothing to shorten, so nothing to measure.

Note we don't rank by line count: we run the proof body through a tokenizer and count tokens (comments and blank lines stripped), so padding with whitespace and comments doesn't help. Existing records run 222–1906 tokens.

2. Expensive to compile

Prefer proofs that burn heartbeats. A proof that costs real elaboration time has real search in it; a cheap one is usually plumbing, and compile cost gives us a second axis to improve besides length. If you can build the project, use #count_heartbeats (under set_option Elab.async false) to find the worst offenders.

3. Unchanged across toolchains

Pick a few toolchain snapshots for the project. The exact declaration text must appear verbatim in a .lean file at every one of them (same bytes, not "an equivalent statement").

Why this matters: tactics, simp sets, and library lemmas shift between Lean releases, so a proof that works at one version may not at another. Holding the statement fixed across versions is what makes the comparison meaningful — any difference in the replayed proof is attributable to the toolchain, not to the theorem having changed. That lets us check whether a shortened proof is genuinely robust or just tuned to one snapshot.

What to send

Email (mike_lu@sfu.ca):

• the fully-qualified declaration name
• the path to the .lean file it lives in
• the commits it's verified at (for cross-version testing)
• the GitHub project URL

Thank you for helping with this — every contribution is much appreciated.