MIRROR of https://codeberg.org/catseye/Philomath : An LCF-style theorem prover written in C89 (a.k.a ANSI C)
Online platform to enable Logic students to write, verify, and store System L style Natural Deduction proofs with real-time proof-checking
MIRROR of https://codeberg.org/catseye/Maxixe : A simple proof checker
KAPPA: Kit of Agents for Proof-checking Papers with a proof Assistant. Checks the proofs in LaTeX papers with Lean 4 and Claude Code agents.
MIRROR of https://codeberg.org/catseye/Eqthy : A simple formalized language for equational proofs
Exposition of an LCF-style theorem prover for propositional logic in a Natural Deduction system
An implementation in Lambda-Prolog of the Minimalist Type Theory
A prototypical proof checker and programming language based on illative combinatory logic
not noq
proof language based on https://en.wikipedia.org/wiki/Sequent_calculus and https://us.metamath.org/.
Continuous Integration system that automatically diagnoses, patches, and validates code issues using AI-powered analysis and formal verification.
a proof checker and model checker for minimal propositional logic
Experimental first-order theorem prover in Rust, with Lean 4 proof checking and TSTP output. Currently supports a restricted, equality-free TPTP CNF fragment.
proof-radar — validity cartography for informal mathematics: per-claim maps of where a result is proven, refuted, empirical, marginal, vacuous, or unprobed, with provenance and coverage.
Independent proof checker for Lean 4
ProofGuard: a checker for first-order logic proofs in TSTP format. Placed 5th at ProoVer 2026 (FLoC 2026, Lisbon).
An executable museum of logic: one system, one evidence file, Zig.
Have a well-defined math problem? This AI agent skill helps you prove or disprove it, and checks the answer in Lean 4 + Mathlib. For Claude Code, Codex, and Antigravity.
Certified frame-first SAT middleware — decide structured regions (2-SAT · GF(2) parity · counting) before CDCL, and independently verify every verdict (model replay · DRAT). A research harness for where SAT hardness lives.
A readable, self-checking CDCL SAT solver, preprocessor and encoding library. Every answer comes with a certificate.
To associate your repository with the proof-checking topic, visit your repo's landing page and select "manage topics."