PyLeaner
A Python interface to the Lean 4 kernel — designed for AI–Lean interactive automated theorem proving and related research. PyLeaner provides a production-ready bridge between Python and Lean's internals.
PyLeaner bridges Python and Lean 4 so AI researchers can query formal proof state, extract theorem definitions, and run parallel proof-checking workloads from Python code.
PyLeaner is a library that lets Python code communicate with Lean 4, a programming language used for writing formal mathematical proofs. Lean 4 can check whether a proof is logically valid, and researchers working on AI systems that generate or verify proofs need a way to connect their Python-based machine learning code to Lean's internals. PyLeaner provides that connection.
The library has two parts. One part is an extension for Lean's language server, which is a background process that Lean uses to analyze code in editors. The extension adds new capabilities to that server so that Python can ask it for things beyond what a standard editor would need. The second part is a Python client that talks to the server, manages multiple server instances at once for parallel workloads, and handles the lower-level details of the communication protocol automatically.
From Python, you can load a Lean file and then ask questions about it. You can extract a structured list of all the definitions, theorems, and other declarations in the file, including their parameter names, types, and bodies. You can ask what proof goals remain at a specific point in a proof, which is useful when an AI system needs to decide what step to take next. You can also retrieve any errors or warnings the Lean compiler reported.
The library manages concurrency through a worker pool. When you have many requests to process, the pool distributes them across multiple running Lean server instances and routes each request to whichever one is least busy. Each operation pairs the step of pushing updated file content to the server with the step of querying the result, so you always get a consistent answer.
PyLeaner does not require Mathlib (the main Lean mathematics library) to be installed, but it works with Mathlib projects. Installation involves adding a dependency in your Lean project and installing the Python package separately with pip.
Where it fits
- Build an AI system that generates proof steps by querying what goals remain at each point in a Lean proof.
- Extract all theorems and definitions from a Lean file into a structured format for training or analysis.
- Run large batches of proof-checking requests in parallel using a managed pool of Lean server instances.
- Retrieve compiler errors from Lean files programmatically inside a Python machine learning pipeline.