Proof assistant/External Links

Please sort and annotate in a user-friendly manner and consider archiving the URLs behind the links you provide. See also related web sources.

Formalizing 100 Theorems

Top 100 theorems in Isabelle

Literature

Some books mentioned on the "Bibliography" page:

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

The Seventeen Provers of the World

Isabelle/Isar

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

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

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)

Wikipedia

WP:Interactive theorem proving

WP:Automated proof checking

WP:Isabelle (theorem prover)

WP:Fold (higher-order function)