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.
A Proof-oriented Programming Language
Lean Theorem Prover
Lean 3's obsolete mathematical components library: please use mathlib4
LLMs as Copilots for Theorem Proving in Lean
CakeML: A Verified Implementation of ML
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.
Tool for data extraction and interacting with Lean programmatically.
Software Foundations in Idris
Bug-free machine learning on stochastic computation graphs
A Learning Environment for Theorem Proving with the Coq proof assistant
Links to tools by subject
ACL2 System and Books as Maintained by the Community
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Retrieval-Augmented Theorem Provers for Lean
Proving Ground: Tools for Automated Mathematics
llmstep: [L]LM proofstep suggestions in Lean 4.
Tableau-based Theorem Prover for Natural Logic and Language
ChatGPT plugin for theorem proving in Lean
Jupyter kernel for Coq
Add a description, image, and links to the theorem-proving topic page so that developers can more easily learn about it.
To associate your repository with the theorem-proving topic, visit your repo's landing page and select "manage topics."