Theorem Proving Python Packages

pyprover

Resolution theorem proving for predicate logic in pure Python.

velaris-lang

Run code an AI wrote without handing it everything you can reach. Each function declares what it may touch. You grant the run one folder, one host or a number of calls, and the runtime refuses anything else the moment it's tried.

certo-math

Between having a mathematical idea and having a proof of it there is a lot of work that is not proving: find the object, break the false claims, measure what survives, reduce it to what it really is, assemble the rest. certo does that work, and every step returns a certificate anyone can re-check without trusting it. CLI + MCP.

isar-tools

Source tooling for Isabelle/Isar projects: a formatter, project and source checks, and statistics.

open-ontologies-lite

Plan, apply and roll back changes to a production ontology, with a blast radius report and a proof an auditor can re-check.

sabline-lang

Run code an AI wrote without handing it everything you can reach. Each function declares what it may touch. You grant the run one folder, one host or a number of calls, and the runtime refuses anything else the moment it's tried.

unicode-fol-kit

Parse, translate, prove and model-check logic formulas in Unicode notation: first-order, modal, description and higher-order logic, one API over a dozen provers, and an MCP server

gonzalgo

Axiom provenance for Lean 4 and Metamath — which step introduced an axiom, and whether the theorem statement required it Website: https://f-keys.com/gonzalgo/

logic-prover

A formal logic theorem prover, formula explorer, deducer, and Lean 4 exporter in Python with Cython acceleration.

lean-dojo

Tool for data extraction and interacting with Lean programmatically.

tensor-theorem-prover

First-order logic theorem prover supporting unification with approximate vector similarity

isabelle-blueprint

Project planning, dependency tracking, and AI-task orchestration for Isabelle formalization projects.

unicode-logic-kit

Parse, translate, prove and model-check logic formulas in Unicode notation: first-order, modal, description and higher-order logic, one API over a dozen provers, and an MCP server

pytactician

An API for interfacing with Coq through Tactician by external agents

tinylean

Tiny theorem prover with syntax like Lean 4 in <1K LOC

open-atp

OpenATP is an open-source Python package providing a common interface for Automated Theorem Proving (ATP)

lean-dojo-v2

LeanDojo-v2 is an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for Lean 4.

mmforge

Find avoidable axiom dependencies in Metamath databases, and build the proofs that remove them. Nine contributions merged into set.mm.

clauz3

Static contract experiments for agent-authored Python

coq-jupyter

Jupyter kernel for Coq

nd-prover

Natural deduction proof generator & checker

lean-probe

Fast Lean 4 proof feedback for coding agents. CLI, Python library, and MCP server with warm LeanInteract sessions and cached env reuse.

knuckledragger

A Low Barrier Proof Assistant

arbiter-debate

Open-source framework for formally verifying academic paper claims using multi-agent LLM debate + Z3/Knuckledragger proof certificates. Supports OpenAI, Anthropic, Google, Grok.