Mining the Archive of Formal Proofs

Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, Tobias Nipkow

The Archive of Formal Proofs is a vast collection of computer-checked proofs developed using the proof assistant Isabelle. We perform an in-depth analysis of the archive, looking at various properties of the proof developments, including size, dependencies, and proof style. This gives some insights into the nature of formal proofs.



author={Jasmin Blanchette and Max Haslbeck and Daniel Matichuk and Tobias Nipkow},
title={Mining the Archive of Formal Proofs},
booktitle={Conference on Intelligent Computer Mathematics (CICM 2015)},
editor={M. Kerber},
note={Invited paper}}