In 1976, Appel and Haiken proposed what is believed to be the first correct proof of the so-called "four color theorem" ; a enhanced version of this proof has been given in 1995 by Robertson, Seymour and Thomas.
What is remarkable is that the first-order formulation of these proofs is too large for human reading and for conventional means of communication (paper, book, hard disk...). However, large parts of these proofs can be understood as computation steps ; it is therefore possible to describe these proofs in a language combining mathematical reasoning and a programming language.
Since Martin-Lof's type theories and their various extensions include a programming language, they are a natural candidate for formalizing the 4-color's proof. I will describe the effort performed to achieve such a formalization in the system Coq.