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.

pdf

BibTeX:

@inproceedings{BlanchetteHMN-CICM15,
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},
publisher=Springer,series=LNCS,volume={9150},pages={3-17},year=2015,
note={Invited paper}}