Lean4 Python Packages

lean-lsp-mcp

Lean Theorem Prover MCP

65K 371 60

leanclient

Python client to interact with the lean4 language server.

58K 44 10

giftpy

GIFT mathematical core - Formally verified constants (Lean 4)

7K 2 0

lean-explore

A search engine for Lean 4 declarations

3K 64 13

lean-dojo

Tool for data extraction and interacting with Lean programmatically.

2K 794 117

watkins-nn

Conservation-law constrained optimization on the golden-ratio simplex

2K 1 0

ax-prover

A Minimal Agent for Automated Theorem Proving

1K 19 1

lean-dojo-v2

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

1K 77 13

kimina-client

Kimina Lean server (+ client SDK)

847 195 33

tinylean

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

583 68 2

kimina-ast-server

Kimina Lean server (+ client SDK)

442 195 33

simpleafier

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

429 2 0

lean-xplore

A search engine for Lean 4 declarations

372 64 13

atomik-core

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

274 1 0

provably

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

272 0 0

kimina-ast-client

Kimina Lean server (+ client SDK)

266 195 33

lean-runner

Deploying High-Performance Lean 4 Server in One Click

180 9 0

kimina

Kimina Lean server (+ client SDK)

163 195 33

jumla

Jumla generates Lean 4 verification datasets from Python code and tests.

152 0 0

iflow-mcp-ooo0ooo-lean-lsp-mcp

Lean Theorem Prover MCP

102 371 60

lean-lldb

an LLDB extension for debugging Lean programs

73 0 0