leanclient

Interact with the Lean 4 language server in Python.

leanclient is a thin Python wrapper around the native Lean 4 language server. It enables interaction with a Lean 4 language server instance running in a subprocess.

Check out the documentation for more information.

Key Features

Interact: Query and change lean files via the LSP.
Thin wrapper: Directly expose the Lean Language Server.
Fast: Typically more than 95% of time is spent waiting.
Parallel: Easy batch processing of files using all your cores.

Quickstart

The best way to get started is to check out this minimal example in Google Colab:

Or try it locally:

Setup a new lean project or use an existing one. See the colab notebook for a basic Ubuntu setup.
Install the package:

pip install leanclient
# Or with uv:
uv pip install leanclient

Example:

import leanclient as lc

# Start a new client, point it to your lean project root (where lakefile.toml is located).
PROJECT_PATH = "path/to/your/lean/project/root/"
client = lc.LeanLSPClient(PROJECT_PATH)

# Query a lean file in your project
file_path = "MyProject/Basic.lean"
diagnostics = client.get_diagnostics(file_path)
print(f"Found {len(diagnostics)} diagnostics")

# Use a SingleFileClient for simplified interaction with a single file.
sfc = client.create_file_client(file_path)

# Get symbols in the file (theorems, definitions, etc.)
symbols = sfc.get_document_symbols()
print(f"File contains {len(symbols)} symbols")

# Get hover information at a specific position
hover = sfc.get_hover(line=10, character=5)
if hover:
    print(f"Hover info: {hover['contents']}")

# Make a change to the document.
change = lc.DocumentContentChange(
    text="-- Adding a comment at the head of the file\n", 
    start=[0, 0], 
    end=[0, 0]
)
sfc.update_file(changes=[change])

# Verify the change (not written to disk, only in LSP memory)
content = sfc.get_file_content()
assert content.startswith("-- Adding a comment")

# Explore module hierarchy (requires .ilean files from built dependencies)
module = client.prepare_module_hierarchy(".lake/packages/mathlib/Mathlib/Init.lean")
imports = client.get_module_imports(module)
print(f"Module {module['name']} has {len(imports)} direct imports")

imported_by = client.get_module_imported_by(module)
print(f"Module is imported by {len(imported_by)} other modules")

Implemented LSP Interactions

See the documentation for more information on:

Opening and closing files.
Updating (adding/removing) code from an open file.
Diagnostic information: Errors, warnings and information.
Goals and term goal.
Hover information.
Document symbols (theorems, definitions, etc).
Semantic tokens, folding ranges, and document highlights.
Locations of definitions and type definitions.
Locations of declarations and references.
Completions, completion item resolve.
Getting code actions, resolving them, then applying the edits.
Get InfoTrees of theorems (includes rudimentary parsing).
Module hierarchy: Get module info, imports, and reverse dependencies.
Interactive diagnostics and widgets (experimental).

Missing LSP Interactions

"Call hierarchy" is currently not reliable.

Might be implemented in the future:

workspace/symbol, workspace/didChangeWatchedFiles, workspace/applyEdit, ...
textDocument/prepareRename, textDocument/rename
$/lean/staleDependency

Potential Features

Better Windows support
Choose between lean --server and lake serve
Automatic testing (lean env setup) for non Debian-based systems

Documentation

Read the documentation at leanclient.readthedocs.io.

Run make docs to build the documentation locally.

Benchmarks

See documentation for more information.

Testing

make install            # Installs python package and dev dependencies with uv
make test               # Run all tests, also installs fresh lean env if not found
make test-profile       # Run all tests with cProfile

Related Projects

Lean LSP Clients

Lean REPLs

License & Citation

MIT licensed. See LICENSE for more information.

Citing this repository is highly appreciated but not required by the license.

@software{leanclient2025,
  author = {Oliver Dressler},
  title = {{leanclient: Python client to interact with the lean4 language server}},
  url = {https://github.com/oOo0oOo/leanclient},
  month = {1},
  year = {2025}
}

Metadata

Release files for leanclient 0.13.2

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for leanclient 0.13.2
File	Size	Uploaded
leanclient-0.13.2.tar.gz	1.2 MB	Aug 19, 2026	Details

Built distribution (wheel)

Table of built distributions (wheels) for leanclient 0.13.2
File	Interpreter	ABI	Platform	Reset
leanclient-0.13.2-py3-none-any.whl 62.1 kB Aug 19, 2026	Python 3	none	any	Details

Total release size: 1.2 MB

Release files / leanclient-0.13.2.tar.gz

Download URL	leanclient-0.13.2.tar.gz
Size	1.2 MB
Tags	Source
SHA-256 checksum How to use checksums	`31aca954f106805bc8cc296beef3a6cc801807e16d485322bfa80881db36892f`
BLAKE2b-256 checksum How to use checksums	`5145a1e22e15a9ba97708ef887126346769d726678a146af0fd72ab7a26568a3`
Upload date	Aug 19, 2026
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`uv/0.7.15`

Release files / leanclient-0.13.2-py3-none-any.whl

Download URL	leanclient-0.13.2-py3-none-any.whl
Size	62.1 kB
Tags	Python 3
SHA-256 checksum How to use checksums	`91cd941506b052f1f7207eebb28b1f7e21ef3f06eb88484f45a370365b8e7236`
BLAKE2b-256 checksum How to use checksums	`15a096312105a3b32ec483dfd66ad221de40db428bb22e021c2b18512c45ab55`
Upload date	Aug 19, 2026
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`uv/0.7.15`