Theorem Proving Python Packages

pyprover

Resolution theorem proving for predicate logic in pure Python.

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

lean-dojo-v2

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

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

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

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.

nd-prover

Natural deduction proof generator & checker

psitip

Python Symbolic Information Theoretic Inequality Prover

jumla

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

pomagma

An inference engine for extensional lambda-calculus