CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
-
Updated
Aug 31, 2026 - OCaml
#
proof-search
Here are 16 public repositories matching this topic...
Language: All
Filter by language
Sort: Most stars
Sort options
A TACtic library for Agda
-
Updated
Sep 14, 2024 - Agda
Proof search for intuitionistic propositional logic using Dyckhoff's LJT.
-
Updated
Nov 27, 2023 - Standard ML
An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.
hpc logic mpi formal-methods propositional-logic tbb modal-logic mathematical-logic theorem-prover proof-engineering proof-search formal-logic metamath proof-theory condensed-detachment proof-complexity hilbert-systems proof-minimization
-
Updated
Aug 7, 2026 - C++
A repo to document candidate solutions for Erdős problems produced via LLM-driven proof search
-
Updated
Apr 21, 2026 - Lean
Guiding Search for Neural Theorem Proving via Proof Progress Prediction
machine-learning theorem-proving rl lean formal-mathematics proof-search lean4 llm progress-prediction
-
Updated
Jan 10, 2026 - Python
horc: Lightweight HORn-Clause Interpreter
logic-programming expert-system horn-clauses proof-search logical-framework foundations-of-mathematics
-
Updated
Sep 11, 2024 - Prolog
ECHIDNA — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance. Neurosymbolic theorem proving with 30 prover backends
theorem-proving formal-verification automated-reasoning proof-search premise-selection neurosymbolic proof-assistants smt-solvers proof-certificates
-
Updated
Sep 7, 2026 - Rust
Crowdfunded automated proof search on open math & CS problems
-
Updated
Aug 27, 2026 - JavaScript
Intuitionistic and classical propositional logic library
propositional-logic natural-deduction proof-search sequent-calculus intuitionistic-logic classical-logic automated-theorem-proving
-
Updated
Jul 12, 2023 - Haskell
Coq implementation of a Gentzen G' propositional sequent prover
-
Updated
Jun 4, 2026 - Rocq Prover
Auditable Codex skill for hard mathematical proofs: proof search, failed-proof recovery, replayable CAS/Lean evidence, and honest proof status.
theorem-proving proof-assistant formal-methods dynamic-programming operations-research symbolic-computation codex bandits wolfram-language learning-theory proof-search mechanism-design wolfram-engine lean4 mathematical-proofs agent-skills codex-skill proof-debugging failed-proof-recovery route-control
-
Updated
Aug 13, 2026 - Python
Typeclass instance resolution as package dependency resolution — a resolution calculus with lazy fixed-point semantics
-
Updated
Mar 1, 2026 - Nix
A local Xiangqi rules, proof, certificate, store, and UCI analysis toolkit
-
Updated
Jul 23, 2026 - Python
Lean theorem prover MCP: automated proof search, mathlib integration, job management
mcp theorem-proving formal-verification proof-search mathlib lean4 lean-language fastmcp alphaproof ai-assisted-proving
-
Updated
Sep 6, 2026 - Python
Add this topic to your repo
To associate your repository with the proof-search topic, visit your repo's landing page and select "manage topics."