Appears in collection : MALINCA Kick-off meeting

Advances in the state of the art in computer-checkable formal proofs has advanced to cover significant mathematical results, such as the Odd Order theorem, the Kepler conjecture, or more recently Carleson's theorem. Tackling such large proofs requires organising the large amount of details necessary for mechanical verification so that they do not obscure the overall flow of the argument. In particular the description of concepts, objects and notations must allow them to mesh and be combined naturally. Modern type theory provides a range of efficient tools for accomplishing this; this talk will cover some of our experience in developing applying these tools to the formalised proofs of Four Colour and Odd Order theorems.