Isabelle

isabelle.in.tum.desite

General-purpose interactive theorem prover with higher-order logic and set-theory environments for formalizing mathematics and computer science.

from

Math

added

2026-10-10

likes

0

similar

1. ▲
   Archive of Formal Proofs isa-afp.org

   site category #math link ↗

   Refereed collection of Isabelle proof libraries, examples, and scientific developments maintained against current Isabelle releases.

2. ▲
   Set Theory and Foundations of Mathematics settheory.net

   site category #math link ↗

   Sylvain Poirier.

3. ▲
   Programs and Proofs ilyasergey.net

   site category #coq link ↗

   Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.

4. ▲
   Knowledge complexity of interactive proof systems github.com

   site category #crypto-papers link ↗
5. ▲
   Itauto gitlab.inria.fr

   site category #coq link ↗

   SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.

   
6. ▲
   MathComp School github.com

   tool category #coq link ↗

   Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library.

   

Math › Foundations and Logic > Formal Mathematics and Theorem Proving: “General-purpose interactive theorem prover with higher-order logic and set-theory environments for formalizing mathematics and computer science.”