Mining the Archive of Formal Proofs
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}}