Lean4 Python Packages

lean-lsp-mcp

Lean Theorem Prover MCP

leanclient

Python client to interact with the lean4 language server.

darm-guard

Runtime authorization for AI agents: a broker executes only what a decision kernel, compiled from a machine-checked Lean 4 model, admits, and leaves signed evidence of every effect.

symkit-mcp

It is an MCP server that lets AI agents perform step-by-step symbolic derivations: calculate, transform, verify, and store formulas with full provenance, all through conversation.

detective-spec

Writes the behavioral contract for a Python function — every behavior pinned by a test, every question it cannot answer named

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.

lean-explore

A search engine for Lean 4 declarations

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.

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.

ax-prover

A Minimal Agent for Automated Theorem Proving

mathlas-mcp

Airtight math tools an AI uses over MCP — 3.7M-theorem search, PSLQ constant ID, OEIS, real Lean kernel checks, applicability checklists. No LLM inside, no API key.

kimina-client

Kimina Lean server (+ client SDK)

xlade

A Lean 4 Ecosystem Framework!

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.

verso-mcp

MCP server to read Verso-generated documentation sites (e.g., the Lean Language Reference)

formulation-bench

Utilities for loading and working with the FormulationBench dataset.

tinylean

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

kimina-ast-server

Kimina Lean server (+ client SDK)

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.

lean-xplore

A search engine for Lean 4 declarations

kimina-ast-client

Kimina Lean server (+ client SDK)