A formal proof is a proof within an axiomatic system, where proof steps are either applications of axioms or applications of formally proven statements. Formal proofs have a long history within mathematics, starting with Euclid’s element’s which had an axiomatic system for geometrical reasoning. The main motivation of constructing a formal proof is obtaining unambiguous detailed proofs that can be mechanically checked. The advent of computer-based tools for formal proof, such as automatic and interactive theorem provers, made it feasible to produce formal versions of proofs that would otherwise be impossible.

A matching in an undirected graph is a subset of the edges of the graph s.t. no two edges are incident on the same vertex. In addition to the rich mathematical structure exhibited by matchings, algorithms to compute matchings have many applications, ranging from matching kidney donors and recipients to the allocation of advertisers to users of search engines.

In this talk, after giving an overview of the state-of-the-art, I will discuss my work on applying formal proof technology to matching theory, discussing some interesting findings and the even more interesting open questions.