Formalizing plane graph theory: towards a formalized proof of the Kepler conjecture. - Gertrud Josefine Bauer (2006)