Proof Assistant Python Packages

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/

giftpy

Certified mathematical identities of the K₇ framework: E₈×E₈ gauge theory on a G₂-holonomy manifold, 460+ relations, 0 sorry, Lean 4. Formerly gift-framework/core (GIFT Core). Distinct from Arithmon/Lean, the Sieve methodology layer.

isabelle-blueprint

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

hypermath-foundations

A closed formal universe derived from one primitive operation, with a Lean translation and a reproducible audit that publishes its own open obligations.

coq-jupyter

Jupyter kernel for Coq

anita

Analytic Tableau Proof Assistant (ANITA) is a tool for teaching Analytic Tableaux

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.

proofs

This is a proofs validator to help students and hobbyists do mathematical thinking and problem solving.

widip

A higher-order computing system

nadia-proof

Natural Deduction Proof Assistant (NADIA) is a tool for teaching Natural Deduction in Fitch-Style