Top 18 theorem-proving open source projects

A Proof-oriented Programming Language

Homepage Theorem Proving in Lean FAQ

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.

No description or website provided.

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Jupyter kernel for Coq

Public code developed during my MSc study at University of Bologna

GAPT: General Architecture for Proof Theory

Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on

An SMT Solver for string constraints

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

An inference engine for extensional untyped λ-calculus

Book: Gentle Introduction to Dependent Types with Idris

Razor is a tool for constructing finite models for first-order theories

Resolution theorem proving for predicate logic in pure Python.