Links:Proof assistant

Formalizing 100 Theorems

Top 100 theorems in Isabelle

Contents 1 Literature 2 Isabelle/Isar 3 Other projects 4 Wikipedia

[edit] Literature

Some books mentioned on the "Bibliography" page:

Nipkow, Paulson, Wenzel: Isabelle/HOL (tutorial) (newer version, of 2010)

The Seventeen Provers of the World

[edit] Isabelle/Isar

Isabelle : Overview, Documentation, Download and installation, Projects, Theory library, Journal

IsarMathLib: A library of formalized mathematics for Isabelle/ZF : Questions and Answers

[edit] Other projects

Mizar : Theory library : Journal

Nuprl: Proof/Program Refinement Logic : Theory library

IMPS, An Interactive Mathematical Proof System : Theory library

Ssreflect (Small Scale Reflection Extension for the Coq system) : Theory library

Coq : Theory library

HOL (history and relatives)

HOL Light

PVS Specification and Verification System

The Proof EditorAlpha

The Theorema System

PhoX

Jape

Prover9 (and Mace4; successor of Otter).

MINLOG

OMEGA

Matita

Twelf

Metamath

Lego (1999)

Mechanized Reasoning (1996)

Database of Existing Mechanized Reasoning Systems (1999)

[edit] Wikipedia

wp:Interactive theorem proving

wp:Automated proof checking

wp:Isabelle (theorem prover)

wp:Fold (higher-order function)