Trustworthy Systems

Mining the archive of formal proofs

Authors

Jasmin Blanchette, Maximilian Haslbeck, Daniel Matichuk and Tobias Nipkow

INRIA
France

Max-Planck-Institute for Computer Science

Technische Universitaet Muenchen
Germany

NICTA

UNSW

Abstract

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.

BibTeX Entry

  @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}
  }

Download