Mathlib 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/

open-atp

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

lean-probe

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

provenance-substrate

The model proposes, deterministic code disposes, a human signs. Content-addressed envelopes, hash-chained audit, signed approval — for ledgers, Lean proofs, manuscript claims, reproductions, benchmarks, peer review. Conformance-tested; byte-compatible with @kernel.chat/kbot-finance.

leanscreen

A calibrated faithfulness screen for informal↔Lean 4 pairs, on the command line and over MCP. Screens only, never certifies.