Pantograph Kernel

lean-py ships a high-level Kernel class that gives Python direct access to Lean’s type-checker, elaborator, and tactic engine. No custom Lean project is needed – any library that imports LeanPy.Kernel already has the full API surface.

View full source on GitHub

Setting up

The Kernel wraps a LeanLibrary. The library just needs to import LeanPy.Kernel and call #export_python_registry:

import LeanPy
import LeanPy.Kernel
#export_python_registry "PantographDemo"

That single file is the entire Lean side. All ~30 kernel functions are pre-registered in LeanPy.Kernel upstream.

On the Python side:

from lean_py import LeanLibrary
from lean_py.kernel import Kernel

lib = LeanLibrary.from_lake("path/to/lean", "PantographDemo", build=True)
k = Kernel(lib)

Loading an environment

Before you can do anything, load one or more Lean modules into the kernel:

>>> k.init_search("")
>>> k.load(["Init"])
>>> k.is_loaded()
True
>>> k.decl_count()
8947

This loads the full Init library – all of Lean’s built-in types, tactics, and notation.

Introspecting declarations

Once the environment is loaded, you can query any declaration:

>>> k.decl_exists("Nat.succ")
True

>>> k.decl_type("Nat.succ")
'Nat → Nat'

>>> k.module_of("Nat.succ")
'Init.Prelude'

catalog() returns all declaration names, search("add") filters by substring.

Running the elaborator

The kernel can elaborate expressions, compute weak-head normal forms, and decide propositions:

>>> k.infer_type("Nat.succ Nat.zero")
'Nat'

>>> k.whnf("(fun x => x + 1) 4")
'5'

>>> k.decide("1 + 1 = 2")
'true'

>>> k.decide("3 < 2")
'false'

parse_type parses a type expression, and expr_echo returns both the elaborated expression and its type.

Creating goals and running tactics

This is the core of the kernel facade. Create a goal from a type string, then apply tactics step by step:

>>> state = k.goal_create("∀ n : Nat, n + 0 = n")
>>> state.n_goals()
1
>>> state.is_solved()
False
>>> print(state.pretty())
⊢ ∀ (n : Nat), n + 0 = n

Apply a tactic:

>>> result = state.try_tactic("intro n")
>>> result.ok
True
>>> print(result.state.pretty())
n : Nat
⊢ n + 0 = n

Each try_tactic call returns a TacticResult with a status ("success" / "failure" / "parseError"), diagnostic messages, and the new GoalState if successful.

Beyond try_tactic, there are prograde tactics for structured proof construction:

result = state.try_have("h", "n = n")     # have h : n = n := ?
result = state.try_let("x", "Nat")        # let x : Nat := ?
result = state.try_define("x", "42")      # let x := 42
result = state.try_draft("Nat.add_zero n")  # may leave sorry subgoals

Frontend processing

You can also process raw Lean source code against the current environment:

>>> k.process("def myFn : Nat := 42\n")
'myFn'

>>> k.find_source_path("Init.Prelude")
'/path/to/.elan/toolchains/.../lib/lean/library/Init/Prelude.lean'

>>> state, msg = k.collect_sorrys("def f : Nat := sorry\n")
>>> state.pretty()  # the sorry becomes a goal
'⊢ Nat'

Goal state lifecycle

Goal states support serialisation and branching:

# Pickle / unpickle
state.pickle("/tmp/goal.bin")
restored = k.goal_unpickle("/tmp/goal.bin")

# Branch and merge
branch = state.try_tactic("intro n").state
merged = state.continue_with(branch)

The full GoalState API is documented in Kernel.

What to take away

The kernel facade lets you drive Lean’s proof engine entirely from Python. The pattern is always:

Kernel(lib) – wrap a LeanLibrary
k.load(["Init"]) – load modules
k.goal_create(...) – create goals
state.try_tactic(...) – apply tactics
state.is_solved() – check completion

This is useful for proof search, tactic synthesis, AI-driven theorem proving, and any workflow where you want programmatic control over the proof state.