This release is a pre-release and may not be stable for production use.
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!
1 maintainer
Metadata
1 maintainer
Release files for pylean 0.0.1a0
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | Provenance | |
|---|---|---|---|---|
| pylean-0.0.1a0.tar.gz | 2.8 kB | Without provenance | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| pylean-0.0.1a0-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 5.7 kB
Release files / pylean-0.0.1a0.tar.gz
| Download URL | pylean-0.0.1a0.tar.gz |
|---|---|
| Size | 2.8 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
91e2ffa3f06d03dbc951b86f87a29bf5d1016b607bc3e1d5651a04738b1702c1
|
|
BLAKE2b-256 checksum How to use checksums |
e1e064aaa1771f90919f3d3e05bd7d8d6446e403d0c4a22e5f0edfc22002cf12
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/6.1.0 CPython/3.9.6
|
Release files / pylean-0.0.1a0-py3-none-any.whl
| Download URL | pylean-0.0.1a0-py3-none-any.whl |
|---|---|
| Size | 2.9 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
f05f580c4d2b5d1785b764fbaf7c0c3e41ba6287ea49d6d6288a01ea81f8e452
|
|
BLAKE2b-256 checksum How to use checksums |
210e41385959cbdcbc30887061913c84fcf86099394d2349f80b1c19b00996df
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/6.1.0 CPython/3.9.6
|
Security for pylean 0.0.1a0
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
No provenance found
None of the files in this release were uploaded with provenance metadata.
A note on package security
PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.
