CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
-
Updated
Jul 9, 2026 - OCaml
#
proof-search
Here are 12 public repositories matching this topic...
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
Jun 28, 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
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
Codex skill for hard theory proofs, proof debugging, route control, and failed-proof recovery
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 codex-skill proof-debugging failed-proof-recovery route-control
-
Updated
Jul 13, 2026 - Python
Correctness-first PyTorch EBMs with FFT circulant layers, tiled Triton mixing, differentiable and Householder transforms, HRR formal-state search, Langevin sampling, and reproducible benchmarks.
benchmark deep-learning pytorch scientific-computing triton fourier formal-methods mcmc householder langevin-dynamics proof-search energy-based-model neuro-symbolic denoising-score-matching hrr structured-matrices circulant-matrix block-circulant differentiable-permutation spherical-langevin
-
Updated
Jul 14, 2026 - Python
Typeclass instance resolution as package dependency resolution — a resolution calculus with lazy fixed-point semantics
-
Updated
Mar 1, 2026 - Nix
Improve this page
Add a description, image, and links to the proof-search topic page so that developers can more easily learn about it.
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."