theorem-proving
There are 220 repositories under theorem-proving topic.
coq/coq
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.
FStarLang/FStar
A Proof-oriented Programming Language
leanprover/lean3
Lean Theorem Prover
leanprover-community/mathlib
Lean 3's obsolete mathematical components library: please use mathlib4
CakeML/cakeml
CakeML: A Verified Implementation of ML
lean-dojo/LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
HOL-Theorem-Prover/HOL
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
lean-dojo/LeanDojo
Tool for data extraction and interacting with Lean programmatically.
idris-hackers/software-foundations
Software Foundations in Idris
dselsam/certigrad
Bug-free machine learning on stochastic computation graphs
princeton-vl/CoqGym
A Learning Environment for Theorem Proving with the Coq proof assistant
johnyf/tool_lists
Links to tools by subject
acl2/acl2
ACL2 System and Books as Maintained by the Community
newca12/awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
siddhartha-gadgil/ProvingGround
Proving Ground: Tools for Automated Mathematics
lean-dojo/ReProver
Retrieval-Augmented Theorem Provers for Lean
kovvalsky/LangPro
Tableau-based Theorem Prover for Natural Logic and Language
wellecks/llmstep
llmstep: [L]LM proofstep suggestions in Lean 4.
gapt/gapt
GAPT: General Architecture for Proof Theory
EugeneLoy/coq_jupyter
Jupyter kernel for Coq
evhub/pyprover
Resolution theorem proving for predicate logic in pure Python.
binghe/informatica-public
Public code developed during my MSc study at University of Bologna
bor0/gidti
Book: Introduction to Dependent Types with Idris
Gbury/dolmen
Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
ml4tp/gamepad
A Learning Environment for Theorem Proving
AthenaFoundation/athena
Athena is a modern, practical language for proof engineering & natural deduction.
choukh/Set-Theory
A formalization of the textbook Elements of Set Theory
salmans/rusty-razor
Razor is a tool for constructing finite models for first-order theories
coq-tactician/coq-tactician
A Seamless, Interactive Tactic Learner and Prover for Coq
tlaplus-workshops/ewd998
Distributed termination detection on a ring, due to Shmuel Safra:
choukh/Baby-Set-Theory
Coq集合论中文教程
leoprover/Leo-III
An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
gpoesia/peano
An environment for learning formal mathematical reasoning from scratch
lemmy/ewd998
Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF
loganrjmurphy/LeanEuclid
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.