# Formalization of some central theorems in combinatorics of finite sets

## TL;DR

This paper provides fully formalized proofs of key combinatorial theorems in finite set theory, including Dilworth's, Mirsky's, Hall's, and Erdős-Szekeres theorems, using the Coq proof assistant.

## Contribution

It introduces a formal framework in Coq for proving fundamental theorems in finite posets, enhancing rigor and reproducibility in combinatorics.

## Key findings

- Formal proofs of Dilworth's and Mirsky's theorems established.
- Proofs of Hall's marriage theorem and Erdős-Szekeres theorem included.
- Developed a reusable library for formalizing finite poset theorems.

## Abstract

We present fully formalized proofs of some central theorems from combinatorics. These are Dilworth's decomposition theorem, Mirsky's theorem, Hall's marriage theorem and the Erd\H{o}s-Szekeres theorem. Dilworth's decomposition theorem is the key result among these. It states that in any finite partially ordered set (poset), the size of a smallest chain cover and a largest antichain are the same. Mirsky's theorem is a dual of Dilworth's decomposition theorem, which states that in any finite poset, the size of a smallest antichain cover and a largest chain are the same. We use Dilworth's theorem in the proofs of Hall's Marriage theorem and the Erd\H{o}s-Szekeres theorem. The combinatorial objects involved in these theorems are sets and sequences. All the proofs are formalized in the Coq proof assistant. We develop a library of definitions and facts that can be used as a framework for formalizing other theorems on finite posets.