Pure Python interaction with Lean 4 theorem prover
Project description
PyLean
Pure Python interaction with Lean 4 theorem prover.
Project Status
This package is under active development. The goal is to provide a Python-first interface to Lean 4 where theorems and proofs are first-class Python objects.
Vision
- Everything is a Python object (theorems, proofs, expressions)
- No file I/O - direct interaction through LSP
- Agent-friendly API for AI/ML applications
- CPMpy-style interaction pattern for theorem proving
Coming Soon
- Object-oriented proof construction
- LSP-based communication with Lean 4
- Integration with existing Lean projects
- MCP server for Claude and other AI assistants
Stay tuned!
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
pylean-0.0.1a0.tar.gz
(2.8 kB
view details)
Built Distribution
Filter files by name, interpreter, ABI, and platform.
If you're not sure about the file name format, learn more about wheel file names.
Copy a direct link to the current filters
File details
Details for the file pylean-0.0.1a0.tar.gz.
File metadata
- Download URL: pylean-0.0.1a0.tar.gz
- Upload date:
- Size: 2.8 kB
- Tags: Source
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/6.1.0 CPython/3.9.6
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
91e2ffa3f06d03dbc951b86f87a29bf5d1016b607bc3e1d5651a04738b1702c1
|
|
| MD5 |
5c6fea46d52d4421525cbb4758235cb7
|
|
| BLAKE2b-256 |
e1e064aaa1771f90919f3d3e05bd7d8d6446e403d0c4a22e5f0edfc22002cf12
|
File details
Details for the file pylean-0.0.1a0-py3-none-any.whl.
File metadata
- Download URL: pylean-0.0.1a0-py3-none-any.whl
- Upload date:
- Size: 2.9 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/6.1.0 CPython/3.9.6
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
f05f580c4d2b5d1785b764fbaf7c0c3e41ba6287ea49d6d6288a01ea81f8e452
|
|
| MD5 |
db0191d0e991297af0563163372383d1
|
|
| BLAKE2b-256 |
210e41385959cbdcbc30887061913c84fcf86099394d2349f80b1c19b00996df
|
