{"id":"palomar/PALOMAR-2026-08-31-000017","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/becacae53c6b6de3322707e130b5829dbbce0ed4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000017-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:06A07","msc:05A18","msc:05D15","combinatorics","order-theory","lean-formalization"],"score":0,"title":"sneed-and-feed/lean-theorems-1","trust":"high","domain":"math.CO","source":"palomar","authors":["Sneed & Feed Formalization Team"],"reviews":0,"subject":"math.CO","summary":"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).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-31","reactions":{},"formalized":true,"formalizes":[{"title":"A Decomposition Theorem for Partially Ordered Sets","identifier":"","relationship":"formalizes"},{"title":"A dual of Dilworth's decomposition theorem","identifier":"","relationship":"formalizes"}]}