MIRROR of https://codeberg.org/catseye/Maxixe : A simple proof checker
MIRROR of https://codeberg.org/catseye/Eqthy : A simple formalized language for equational proofs
ProofGuard: a checker for first-order logic proofs in TSTP format. Placed 5th at ProoVer 2026 (FLoC 2026, Lisbon).
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.
Explain small RUP additions with assumptions, unit reasons and a final-empty-clause requirement.
Replayable Python protocol engine for checking time-bound future claims from canonical artifacts, with typed outcomes and audit trails.
AI-assisted desktop app for auditing mathematical manuscripts, detecting proof issues, and generating reports.
A reproducible audit harness for mathematical LaTeX papers: deterministic scanner, schema-validated issue ledgers with mechanical quote verification, and a stage-gated final gate — driven by any MCP agent or the CLI.
Check DRAT/DRUP proofs of unsatisfiability inside your Python process. Zero dependencies, optional Rust accelerator.
Euclid's Elements as software that runs: every proposition draws its own figure, checks its own conclusion in exact arithmetic, and reports what it depended on.
To associate your repository with the proof-checking topic, visit your repo's landing page and select "manage topics."