Skip to main content
CSIRO Logo Data 61 logo

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,
    author           = {Blanchette, Jasmin and Haslbeck, Maximilian and Matichuk, Daniel and Nipkow, Tobias},
    editor           = {{Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge}},
    month            = jul,
    year             = {2015},
    keywords         = {isabelle afp},
    address          = {Washington DC, USA},
    title            = {Mining the Archive of Formal Proofs},
    pages            = {3--17},
    booktitle        = {Conference on Intelligent Computer Mathematics},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/8734.pdf},
    publisher        = {Springer},
    isbn             = {978-3-319-20614-1}
  }

Download