Metadata-Version: 2.4
Name: pylean
Version: 0.0.1a0
Summary: Pure Python interaction with Lean 4 theorem prover
Author-email: Stefan Szeider <stefan@szeider.net>
License: MIT
Project-URL: Homepage, https://github.com/yourusername/pylean
Project-URL: Bug Reports, https://github.com/yourusername/pylean/issues
Project-URL: Source, https://github.com/yourusername/pylean
Keywords: lean,theorem-proving,mathematics,formal-verification
Classifier: Development Status :: 1 - Planning
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Dynamic: license-file

# 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!
