semvec/pypi-packages huggingface dataset:
pylean 0.0.1a0
Pure Python interaction with Lean 4 theorem prover
License: MIT
Requires Python: >=3.11
Keywords: lean, theorem-proving, mathematics, formal-verification

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