proof-search

CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory

A TACtic library for Agda

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

Proof search for intuitionistic propositional logic using Dyckhoff's LJT.

LLM-driven proof search on Erdős problems (2 solutions accepted on erdosproblems.com)

Gentzen propositional LK sequent calculus automated proof search engine for structural proof theory

Gentzen propositional LK sequent calculus automated proof search engine for structural proof theory

Guiding Search for Neural Theorem Proving via Proof Progress Prediction

horc: Lightweight HORn-Clause Interpreter

Crowdfunded automated proof search on open math & CS problems

Lean theorem prover MCP: automated proof search, mathlib integration, job management

Intuitionistic and classical propositional logic library

Coq implementation of a Gentzen G' propositional sequent prover

Mathematical discovery and proof workflows with durable recovery, explicit evidence scopes, and optional CAS/Lean verification.

Typeclass instance resolution as package dependency resolution — a resolution calculus with lazy fixed-point semantics

A local Xiangqi rules, proof, certificate, store, and UCI analysis toolkit

A linear logic suite: decides, checks, proves step by step and exports sequents of classical and intuitionistic linear logic, with proofs an independent checker validates