Setting Up a Project

This guide walks through creating a new project that uses lean-py from scratch. By the end you will have a Lean library that exports functions, structures, and inductives to Python with full type marshalling.

Directory Layout

A typical lean-py project has two halves – a Lake project for Lean and a pyproject.toml for Python:

my-project/
  lean/
    lakefile.toml
    lean-toolchain
    MyLib.lean
  python/
    pyproject.toml
    main.py

Step 1: Create the Lean Project

mkdir -p my-project/lean && cd my-project/lean
lake init MyLib

Set the toolchain to match lean-py’s pinned version:

echo "leanprover/lean4:v4.29.1" > lean-toolchain

Edit lakefile.toml:

[package]
name = "MyLib"
version = "0.1.0"
leanOptions = []

[[require]]
name = "LeanPy"
git  = "https://github.com/BasisResearch/lean.py"

[[lean_lib]]
name = "MyLib"
moreLinkObjs = [
  "LeanPy/LeanPy:static",
  "LeanPy/leanPyNative:static",
  "Pantograph/Pantograph:static",
]
precompileModules = true
defaultFacets = ["shared"]
moreLinkArgs = ["-Wl,-headerpad_max_install_names"]

Step 2: Write Lean Code

Create MyLib.lean:

import LeanPy
open LeanPy

-- Export a simple function
@[python "increment"]
def increment (n : Int) : Int := n + 1

-- Export a structure
structure Point where
  x : Int
  y : Int

derive_python Point

@[python "origin"]
def origin (_ : Unit) : Point := { x := 0, y := 0 }

@[python "norm_sq"]
def normSq (p : Point) : Int := p.x * p.x + p.y * p.y

-- Export an inductive
inductive Shape where
  | circle (radius : Int)
  | rect (width height : Int)

derive_python Shape

@[python "area"]
def area (s : Shape) : Int :=
  match s with
  | .circle r => 3 * r * r     -- approximate
  | .rect w h => w * h

-- Make the registry visible to Python
#export_python_registry "MyLib"

Key concepts:

@[python "name"] marks a function for export with the given symbol name.
derive_python T registers a type’s constructors so Python can create and destructure values of type T.
#export_python_registry "Prefix" emits the JSON metadata that Python reads at load time.

Step 3: Build

cd lean && lake build

This fetches LeanPy and Pantograph, compiles everything, and produces a shared library at lean/.lake/build/lib/libMyLib.{dylib,so}.

Step 4: Create the Python Project

cd ../python
cat > pyproject.toml << 'EOF'
[project]
name = "my-project"
version = "0.1.0"
requires-python = ">=3.12"
dependencies = ["lean_py @ git+https://github.com/BasisResearch/lean.py"]

[build-system]
requires = ["hatchling"]
build-backend = "hatchling.build"
EOF

Install:

uv sync

Step 5: Call Lean from Python

Create main.py:

from lean_py import LeanLibrary

lib = LeanLibrary.from_lake("../lean", "MyLib")

# Functions
print(lib.increment(41))        # 42

# Structures
p = lib.Point(3, 4)
print(p)                        # Point.mk(3, 4)
print(lib.norm_sq(p))           # 25

# Inductives
c = lib.Shape.circle(5)
r = lib.Shape.rect(3, 4)
print(lib.area(c))              # 75
print(lib.area(r))              # 12

Run:

uv run python main.py

Using Additional Lake Dependencies

If your Lean code depends on other libraries (Batteries, Mathlib, etc.), add them as [[require]] entries and include them in moreLinkObjs if their symbols are called at runtime:

[[require]]
name = "batteries"
git  = "https://github.com/leanprover-community/batteries"
rev  = "main"

[[lean_lib]]
name = "MyLib"
moreLinkObjs = [
  "LeanPy/LeanPy:static",
  "LeanPy/leanPyNative:static",
  "Pantograph/Pantograph:static",
  "batteries/Batteries:static",
]

Rule of thumb: if lake build succeeds but Python fails with symbol not found, add the missing package as "<package>/<LibName>:static" to moreLinkObjs.

Type Marshalling Reference

lean-py automatically marshals these types between Lean and Python:

Lean type	Python type	Notes
`Unit`	`None`
`Bool`	`bool`
`Nat`	`int`	Non-negative
`Int`	`int`
`Float`	`float`
`String`	`str`
`Char`	`str` (length 1)
`UInt8/16/32/64`	`int`
`Array a`	`list`
`List a`	`list`
`Option a`	value or `None`
`a x b`	`tuple`
`IO a`	unwrapped value	Raises `LeanError` on error
User inductives	`LeanInductiveValue`	Via `derive_python`
User structures	`LeanInductiveValue`	Callable constructor

Pattern Matching on Inductives

Constructor classes on inductive type namespaces support Python 3.10+ structural pattern matching via __match_args__:

Shape = lib.Shape

match lib.area_input():
    case Shape.circle(radius):
        print(f"circle: pi * {radius}^2")
    case Shape.rect(w, h):
        print(f"rect: {w} * {h}")

Each constructor class also works with isinstance:

val = lib.Shape.circle(5)
assert isinstance(val, Shape.circle)     # True
assert not isinstance(val, Shape.rect)   # True

For enum-like inductives (all nullary constructors), the classes still work as values for backward compatibility:

Color = lib.Color
lib.colorId(Color.red)  # 0