This is an unofficial reimagining of the Archive of Formal Proofs
Flyspeck I: Tame Graphsby Gertrud Bauer and Tobias Nipkow