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

lean-dojo

Tool for data extraction and interacting with Lean programmatically.

goodhart

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

ax-prover

A Minimal Agent for Automated Theorem Proving

watkins-nn

Conservation-law constrained optimization on the golden-ratio simplex

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. 33 backends (software · GPU shaders · FPGA · Lean proofs · safety-critical) from one source, with chain-order analysis and Lean-checkable contracts on every function.

lean-probe

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

kimina-client

Kimina Lean server (+ client SDK)

tinylean

Tiny theorem prover with syntax like Lean 4

simpleafier

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

kimina-ast-server

Kimina Lean server (+ client SDK)

atomik-core

ATOMiK delta-state algebra — O(1) state reconstruction for any processor

lean-xplore

A search engine for Lean 4 declarations

kimina-ast-client

Kimina Lean server (+ client SDK)

provably

Proof-carrying Python functions via Z3 — annotate, verify, ship.

jumla

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

lean-runner

Deploying High-Performance Lean 4 Server in One Click

kimina

Kimina Lean server (+ client SDK)

iflow-mcp-ooo0ooo-lean-lsp-mcp

Lean Theorem Prover MCP

lean-lldb

an LLDB extension for debugging Lean programs