# 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!
Raw data
{
"_id": null,
"home_page": null,
"name": "pylean",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.11",
"maintainer_email": null,
"keywords": "lean, theorem-proving, mathematics, formal-verification",
"author": null,
"author_email": "Stefan Szeider <stefan@szeider.net>",
"download_url": "https://files.pythonhosted.org/packages/e1/e0/64aaa1771f90919f3d3e05bd7d8d6446e403d0c4a22e5f0edfc22002cf12/pylean-0.0.1a0.tar.gz",
"platform": null,
"description": "# PyLean\n\nPure Python interaction with Lean 4 theorem prover.\n\n## Project Status\n\nThis 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.\n\n## Vision\n\n- Everything is a Python object (theorems, proofs, expressions)\n- No file I/O - direct interaction through LSP\n- Agent-friendly API for AI/ML applications\n- CPMpy-style interaction pattern for theorem proving\n\n## Coming Soon\n\n- Object-oriented proof construction\n- LSP-based communication with Lean 4\n- Integration with existing Lean projects\n- MCP server for Claude and other AI assistants\n\nStay tuned!\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "Pure Python interaction with Lean 4 theorem prover",
"version": "0.0.1a0",
"project_urls": {
"Bug Reports": "https://github.com/yourusername/pylean/issues",
"Homepage": "https://github.com/yourusername/pylean",
"Source": "https://github.com/yourusername/pylean"
},
"split_keywords": [
"lean",
" theorem-proving",
" mathematics",
" formal-verification"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "210e41385959cbdcbc30887061913c84fcf86099394d2349f80b1c19b00996df",
"md5": "db0191d0e991297af0563163372383d1",
"sha256": "f05f580c4d2b5d1785b764fbaf7c0c3e41ba6287ea49d6d6288a01ea81f8e452"
},
"downloads": -1,
"filename": "pylean-0.0.1a0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "db0191d0e991297af0563163372383d1",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.11",
"size": 2919,
"upload_time": "2025-08-05T08:45:44",
"upload_time_iso_8601": "2025-08-05T08:45:44.057296Z",
"url": "https://files.pythonhosted.org/packages/21/0e/41385959cbdcbc30887061913c84fcf86099394d2349f80b1c19b00996df/pylean-0.0.1a0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "e1e064aaa1771f90919f3d3e05bd7d8d6446e403d0c4a22e5f0edfc22002cf12",
"md5": "5c6fea46d52d4421525cbb4758235cb7",
"sha256": "91e2ffa3f06d03dbc951b86f87a29bf5d1016b607bc3e1d5651a04738b1702c1"
},
"downloads": -1,
"filename": "pylean-0.0.1a0.tar.gz",
"has_sig": false,
"md5_digest": "5c6fea46d52d4421525cbb4758235cb7",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.11",
"size": 2822,
"upload_time": "2025-08-05T08:45:45",
"upload_time_iso_8601": "2025-08-05T08:45:45.544183Z",
"url": "https://files.pythonhosted.org/packages/e1/e0/64aaa1771f90919f3d3e05bd7d8d6446e403d0c4a22e5f0edfc22002cf12/pylean-0.0.1a0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-08-05 08:45:45",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "yourusername",
"github_project": "pylean",
"github_not_found": true,
"lcname": "pylean"
}
JSON
