Open Research Index

sneed-and-feed/lean-theorems-1

Sneed & Feed Formalization Team

Palomar Registrypalomar/PALOMAR-2026-08-31-000017Aug 31, 2026math.COscore 0

A complete, machine-checked Lean 4 formalization of Dilworth's Theorem (Robert P. Dilworth, 1950) on chain decompositions of finite posets and Mirsky's Dual Theorem (Leon Mirsky, 1971) on antichain covers. Proves that the maximum size of an antichain equals the minimum number of chains covering the poset, and dually that the maximum length of a chain equals the minimum number of antichains covering the poset. To the maintainers' knowledge, the theorem was not found in an exact declaration name, docstring, and type signature search of the pinned Mathlib revision (Mathlib v4.34.0-rc1).

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-31-000017
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-31-000017/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-31-000017/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'