Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar). - Gertrud Bauer; Markus Wenzel 001 (TYPES, 1999)

Calculational Reasoning Revisited (An Isabelle/Isar Experience). - Gertrud Bauer; Markus Wenzel 001 (TPHOLs, 2001)

The 5 Colour Theorem in Isabelle/Isar. - Gertrud Bauer; Tobias Nipkow (TPHOLs, 2002)

Towards a Verified Enumeration of All Tame Plane Graphs. - Tobias Nipkow; Gertrud Bauer (Mathematics, Algorithms, Proofs, 2005)

Flyspeck I: Tame Graphs. - Tobias Nipkow; Gertrud Bauer; Paula Schultz (IJCAR, 2006)

Flyspeck I: Tame Graphs. - Gertrud Bauer; Tobias Nipkow (Arch. Formal Proofs, 2006)

A formal proof of the Kepler conjecture. - Thomas C. Hales; Mark Adams; Gertrud Bauer; Dat Tat Dang; John Harrison 001; Truong Le Hoang; Cezary Kaliszyk; Victor Magron; Sean McLaughlin; Thang Tat Nguyen; Truong Quang Nguyen; Tobias Nipkow; et al. (CoRR, 2015)