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.
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.
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.
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.
Explain small RUP additions with assumptions, unit reasons and a final-empty-clause requirement.
Eyedia — reasoning you can see. A dependency-free Prolog rule language with forward and backward reasoning, where every answer can come with a proof you can check.
Replayable Python protocol engine for checking time-bound future claims from canonical artifacts, with typed outcomes and audit trails.
To associate your repository with the proof-checking topic, visit your repo's landing page and select "manage topics."