Bend 2: a fast language that blocks AI mistakes via proof. Install: curl -fsSL https://bend-lang.com/install.sh | sh
-
Updated
Nov 12, 2026 - TypeScript
#
theorem-proving
Here are 1,037 public repositories matching this topic...
The Rocq Prover is an interactive theorem prover, or proof assistant. 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.
-
Updated
Nov 12, 2026 - OCaml
A Proof-oriented Programming Language
programming-language dependent-types ocaml theorem-proving verification f-sharp proof-assistant smt c-language fstar interactive-theorem-proving program-proof dijkstra-monads
-
Updated
Nov 12, 2026 - F*
Formal verification for AI: a Lean 4 + Dafny proof checker that catches fake AI proofs (reward hacking), and verified recursive self-improvement (RSI) for coding agents. AI for math, physics and software engineering.
theorem-proving proof-assistant formal-methods dafny program-verification formal-verification ai-safety rsi ai-agents automated-theorem-proving lean4 llm ai-for-science recursive-self-improvement coding-agents autoformalization self-improving-ai reward-hacking ai-for-math verified-code
-
Updated
Oct 22, 2026 - Python
Plan, apply and roll back changes to a production ontology, with a blast radius report and a proof an auditor can re-check.
rust sparql mcp theorem-proving owl ontology knowledge-graph lean infrastructure-as-code formal-verification description-logics shacl reasoning owl2 lean4 ai-native isabelle-language mcp-server
-
Updated
Nov 12, 2026 - Rust
Lean Theorem Prover
-
Updated
Oct 14, 2023 - C++
Lean 3's obsolete mathematical components library: please use mathlib4
-
Updated
Nov 6, 2026 - Lean
LLMs as Copilots for Theorem Proving in Lean
-
Updated
Oct 13, 2026 - C++
CakeML: A Verified Implementation of ML
-
Updated
Nov 12, 2026 - Standard ML
An Axum-based Rust web framework with Lean 4-verifiable application kernels that run on servers, bare-metal embedded devices, and GPUs, plus integrated security testing.
embedded theorem-proving verification hacking web-framework embedded-systems webapp cybersecurity penetration-testing gpu-acceleration web-security cuda-kernels offensive-security formal-verification ethical-hacking red-team ai-safety gpu-programming ai-security lean4
-
Updated
Nov 12, 2026 - Rust
Tool for data extraction and interacting with Lean programmatically.
-
Updated
Jan 18, 2026 - Python
A project to digitalise results from physics into Lean.
-
Updated
Nov 12, 2026 - Lean
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.
-
Updated
Nov 12, 2026 - Standard ML
Software Foundations in Idris
-
Updated
May 15, 2019 - Idris
ACL2 System and Books as Maintained by the Community
common-lisp logic theorem-proving first-order-logic formal-methods formal-verification theorem-prover rewriting acl2
-
Updated
Nov 12, 2026 - Common Lisp
A Learning Environment for Theorem Proving with the Coq proof assistant
-
Updated
Jun 30, 2023 - Coq
Bug-free machine learning on stochastic computation graphs
-
Updated
Mar 3, 2019 - Lean
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
rust dependent-types logic theorem-proving formal-verification prover automated-theorem-provers reasoning theorem-prover constructive-mathematics proof-assistants
-
Updated
Nov 7, 2026
Links to tools by subject
tools static-analysis theorem-proving verification proof-assistant smtlib synthesis satisfiability-solver binary-decision-diagrams model-checking satisfiability-modulo-theories formal-methods theorem-prover
-
Updated
Mar 19, 2024
Composable mathematics tools for agents
python math computer-algebra mcp theorem-proving proof-assistant formal-methods sympy formal-verification dsh erdos symbolic-math ai-agents cordis automated-theorem-proving lean4 model-context-protocol mcp-server erdos-problem dsh-plugin
-
Updated
Nov 9, 2026 - Python
Add this topic to your repo
To associate your repository with the theorem-proving topic, visit your repo's landing page and select "manage topics."