Lean evidence record
Dilworth’s Theorem: Lean evidence
This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.
Exact recorded Lean statement
The declaration this evidence supports
theorem dilworthTheorem : DilworthTheoremStatementLine counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Technical evidence record
Source identity, checker results, and assumptions
- Main Lean declaration
dilworthTheorem- Source commit
56a5eacbfd70
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.known-dilworth-theorem.endpoint.v001- Accepted-result title
- Accepted Result: Dilworth’s Theorem
- Accepted-result status
- Accepted formalization of a known theorem
- Accepted-result boundary
- For every finite partially ordered type, if every antichain has size at most k, then k chains cover all elements. Non-claim: The endpoint records a cover indexed by Fin k; it does not literally state a disjoint partition or the min-max equality between width and the least number of chains.
- Declarations covered by recorded evidence
AtlasKnownTheorems.DilworthTheorem.dilworthTheoremAtlasKnownTheorems.DilworthTheorem.DilworthTheoremStatement- Lean build
- passed
- Recorded build time
- 4.3 s one machine-dependent evidence run, not a benchmark
- Evidence collected
- · clean-source provenance recorded
- Unfinished proof check
- passed
- Lean toolchain
leanprover/lean4:v4.29.1- Recorded source commit
56a5eacbfd70c6e6a05b23003f9aad9936fb9f6e- Source SHA-256
sha256:4e4eb174e65cd22cfbad5e0d39d71b56996c9fc8b6d123171a0bc1856fb6a993- Statement alignment
- accepted
Lean foundations
Standard foundations used by the proof
Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.
Classical.choiceQuot.soundpropext
Files and machine-readable evidence
Reproduce or inspect the recorded check
Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.
Review results
Publication reviews accepted
All four required publication-review gates are accepted for the reviewed presentation of this exact theorem. The review results are separate from the Lean build and do not broaden the formal statement.
Read the publication-review details