skip to content

Mining the Archive of Formal Proofs

Presented by: 
Tobias Nipkow Technischen Universität München
Thursday 13th July 2017 - 10:00 to 11:00
INI Seminar Room 1


Co-authors: Jasmin Christian Blanchette (Vrije Universiteit Amsterdam), Maximilian Haslbeck (Technical University Munich), Daniel Matichuk (Data61)
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.

Related Links


Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons