lean-py

Effortless interop between Lean 4 and Python, in both directions.

• Lean -> Python. Annotate any Lean definition with @[python "name"] and call it from Python with automatic type marshalling. derive_python exposes inductives and structures as Python constructors.

• Python -> Lean. LeanPy.Python gives Lean code a Py type with import_, eval, exec, getAttr, call, etc. CPython is loaded lazily via dlopen.

• Kernel facade. LeanPy.Kernel wraps the Pantograph library so a Python process can drive Lean’s type-checker, elaborator, and tactic engine without spawning a subprocess.

Getting Started

• Getting Started
• Setting Up a Project

Examples

• Basic Example
• Pantograph Kernel
• Typed NumPy
• SymPy Tactic
• Z3 / Knuckledragger Tactic
• Effectful Refinement-Type Verifier

API Reference

• Library Loading
  • Loading from a Lake project
  • What happens at load time
  • Calling functions
  • Working with types
  • API reference
• Kernel
  • Setup
  • Loading an environment
  • Querying declarations
  • Elaboration
  • Creating goals and running tactics
  • Goal state lifecycle
  • Environment serialisation
  • Frontend processing
  • API reference
• Marshalling
  • How values cross the boundary
  • LeanObj — owned pointers
  • LeanInductiveValue — Python-side inductives
  • Smart constructors
  • The Marshaller class
  • API reference
• Registry
  • Where the data comes from
  • TypeRepr — describing Lean types
  • CtorInfo — constructor metadata
  • TypeInfo — type metadata
  • FuncInfo — function metadata
  • LibraryRegistry — the full picture
  • API reference
• Exceptions
  • LeanError
  • LeanPyCallbackError
  • API reference

Indices and Tables

• Index

• Module Index

• Search Page