INRIA
France
Max-Planck-Institute for Computer Science
Technische Universitaet Muenchen
Germany
NICTA
UNSW
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.
@inproceedings{Blanchette_HMN_15, address = {Washington DC, USA}, author = {Blanchette, Jasmin and Haslbeck, Maximilian and Matichuk, Daniel and Nipkow, Tobias}, booktitle = {Conference on Intelligent Computer Mathematics}, editor = {{Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge}}, isbn = {978-3-319-20614-1}, keywords = {isabelle afp}, month = jul, pages = {3--17}, paperurl = {https://trustworthy.systems/publications/nicta_full_text/8734.pdf}, publisher = {Springer}, title = {Mining the Archive of Formal Proofs}, year = {2015} }