Lean4 Python Packages

leanclient

Python client to interact with the lean4 language server.

lean-lsp-mcp

Lean Theorem Prover MCP

giftpy

GIFT Core: Certified mathematical identities from E8×E8 gauge theory on G2 manifolds. Verified in Lean 4

lean-explore

A search engine for Lean 4 declarations

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

Client SDK to interact with Kimina Lean server.

lean-dojo

Tool for data extraction and interacting with Lean programmatically.

ax-prover

A Minimal Agent for Automated Theorem Proving

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)

watkins-nn

Watkins Temperature Theorem: conservation-law constrained optimization on the golden-ratio simplex

scpn-mif-core

SCPN MIF-Core — pulsed field-reversed-configuration kinematic and sub-50 ns RTL hot-path laboratory for magneto-inertial fusion control

lean-dojo-v2

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

monogate-forge

EML language and compiler for verified mathematical computation across 36 targets: software, GPU shaders, hardware (FPGA/ASIC, SPICE, KiCad, and JLCPCB), formal verification, and safety-critical systems.

kimina-ast-server

Kimina Lean server (+ client SDK)

simpleafier

Command line tool to help improve the quality of Lean code by converting any "simp" to "simp only".

tinylean

Tiny theorem prover with syntax like Lean 4

verso-mcp

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

xlade

eXperimental Lean 4 advanced Development ecosystem

lean-xplore

A search engine for Lean 4 declarations

atomik-core

Delta-state algebra — O(1) state reconstruction, 99% bandwidth reduction, formally proven with 92 Lean4 theorems. pip install atomik-core | C99 header | FPGA hardware (69.7 Gops/s)

goodhart

Catch reward traps before training. Named after Goodhart's Law.

lean-runner

A Python client for the Lean Theorem Prover Server API.

provably

Proof-carrying Python — Z3-backed formal verification via @verified decorators