Bend 2: a fast language that blocks AI mistakes via proof. Install: curl -fsSL https://bend-lang.com/install.sh | sh
-
Updated
Oct 21, 2026 - TypeScript
#
theorem-proving
Here are 905 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
Oct 21, 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
Oct 21, 2026 - F*
Lean Theorem Prover
-
Updated
Oct 14, 2023 - C++
Lean 3's obsolete mathematical components library: please use mathlib4
-
Updated
Jun 28, 2024 - Lean
LLMs as Copilots for Theorem Proving in Lean
-
Updated
Oct 13, 2026 - C++
CakeML: A Verified Implementation of ML
-
Updated
Oct 21, 2026 - Standard ML
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
Oct 17, 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
Oct 21, 2026 - Lean
An Axum-based Rust web framework for building and verifying web apps with Lean 4, featuring optional GPU acceleration and integrated development infrastructure for red-teaming and CI/CD.
theorem-proving hacking web-framework cybersecurity penetration-testing gpu-acceleration bug-bounty web-security ctf cuda-kernels offensive-security formal-verification ethical-hacking red-team ai-safety gpu-programming ai-security lean4 ai-hacking security-automaion
-
Updated
Oct 21, 2026 - Rust
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
Oct 20, 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
Oct 21, 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
May 27, 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
Retrieval-Augmented Theorem Provers for Lean
-
Updated
Jan 30, 2025 - Python
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
Oct 19, 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."