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.

Theorems

• 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)