While this submission is a draft, it cannot be used by other submissions.

Proof network stress test

lax-771644·formalized by Jan Dreier·created ·GitHub @6f04fdd·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    This submission contains no mathematics of its own. It is a synthetic benchmark for the archive website's proof-network drawing: a submission whose only purpose is to exhibit, in one place and under stable names, every shape that figure has to lay out.

    Every statement here is one rung of a single trivial ladder. StageknStage k n means that nn is divisible by 2k2^k, and each of the 53 statements asserts DescentabDescent a b, that divisibility by 2a2^a implies divisibility by 2b2^b for some concrete aba \ge b. All of them are true, and every proof genuinely applies the statements it declares as assumptions — the mathematics is just thin enough that the dependency graph can be wired into any shape at all.

    The 30 concepts are named after the shapes they exercise: sibling proofs whose conclusion sits at the left, the middle and the right of a dock row; a proof mixing a sibling assumption with a foreign one; chains of sibling proofs; a statement with two proofs and another with three; a twelve-dock concept with an eleven-wide assumption rail; a proof assuming one statement from each of eight other concepts; a genuine two-concept cycle and a one-element self-cycle, both of which stay unproven; an open statement with an open chain below it; nine single-statement concepts in a linear chain; an isolated concept with no edges at all; deliberately overlong and non-ASCII names; and two statements discharged from lax242665lax-242665, so that external nodes appear as well.

    Nothing here should be cited, endorsed or built upon. It is a ruler.

    Concepts

    Concept map
    31 concepts
    100%
    Proven claimOpen claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimOpen claimStatement 1, 2, … of a claim with several statementsClaim from this submission / another submissionProof — open large view for detailsCycle — claims proving each other
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on AA → B: only B's proofs build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-771644,
      author = {Jan Dreier},
      title = {Proof network stress test},
      year = {2026},
      howpublished = {Lax Archive, lax-771644},
      url = {https://laxarchive.org/lax-771644/},
      note = {draft},
    }

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…