Theorem Proving Python Packages

pyprover

Resolution theorem proving for predicate logic in pure Python.

isabelle-blueprint

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

lean-dojo

Tool for data extraction and interacting with Lean programmatically.

lean-probe

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

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.

tensor-theorem-prover

Customizable first-order logic theorem prover supporting approximate vector similarity in unification

knuckledragger

A Low Barrier Proof Assistant

clauz3

Static contract experiments for agent-authored Python

tinylean

Tiny theorem prover with syntax like Lean 4

coq-jupyter

Coq kernel for Jupyter

pytactician

An API for interfacing with Coq through Tactician by external agents

psitip

Python Symbolic Information Theoretic Inequality Prover

arbiter-debate

Formally verified multi-agent debates

nd-prover

Natural deduction proof generator & checker

jumla

Jumla is a Python package for generating Lean 4 formal verification tasks from Python specifications.

pomagma

An inference engine for extensional lambda-calculus