Mathematical proofs when written in conventional ways often contain imprecise definitions, unstated background assumptions, and inferential gaps in reasoning. In such circumstances, it becomes difficult for a reviewer to determine whether the given proof is correct or not. Even if the theorem statement turns out to be true, judging it to be so could take a long time. A possible solution to this problem is to formalize mathematical results using Proof Assistants. Proof Assistants are software tools built on top of a small and trusted kernel that provides a formal language for writing mathematical statements and their proofs. Hence, formally verifying a mathematical theory using a Proof Assistant can increase our confidence in the verified results. However, the task of formalizing mathematics using Proof Assistants presents some unique challenges; both practical as well as theoretical. Theoretical challenges mostly arise because some trivially assumed axioms of classical mathematics may not be provable in the core logic of the Proof Assistant. On the other hand, the practical difficulties of formalization mostly arise because the machine-checkable proofs are significantly more detailed than the corresponding paper proofs. In this talk, we will address both these issues while presenting formal proofs of some key results from finite set combinatorics. More precisely, we present formalized libraries of definitions and results on two important mathematical structures from combinatorics: (i) finite partially ordered sets, and (ii) finite simple graphs. These libraries have been formalized in the type theory of Coq Proof Assistant.
