Kernel

The kernel module gives Python direct access to Lean 4’s type-checker, elaborator, and tactic engine. It wraps ~30 @[python] functions from LeanPy.Kernel into two classes: Kernel (the environment facade) and GoalState (an opaque proof state handle).

Source: lean_py/kernel.py

Setup

Any Lean project that imports LeanPy.Kernel automatically has the kernel surface available. On the Python side:

from lean_py import LeanLibrary
from lean_py.kernel import Kernel

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

Loading an environment

Before any queries, load one or more Lean modules:

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

init_search sets the search path (empty string uses the default toolchain path). load imports one or more modules — pass ["Init", "Mathlib.Tactic.Omega"] to get multiple.

Querying declarations

Once loaded, the full Lean environment is queryable:

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

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

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

>>> k.search("add_comm")
['Nat.add_comm', 'Int.add_comm', ...]

catalog() returns all declaration names. all_decls() returns them including internal names. decl_value retrieves the definition body.

Elaboration

The kernel can elaborate, reduce, and decide:

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

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

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

expr_echo returns both the elaborated expression and its type:

>>> expr, ty = k.expr_echo("(1 : Int) + 1")
>>> expr
'@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) ...'
>>> ty
'Int'

This is useful for discovering the fully-elaborated form of Lean expressions — for instance, the exact instance names needed when building Lean.Expr trees programmatically.

Creating goals and running tactics

This is the heart 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
>>> result.status
'success'
>>> print(result.state.pretty())
n : Nat
⊢ n + 0 = n

Close the proof:

>>> result2 = result.state.try_tactic("simp")
>>> result2.state.is_solved()
True

Failed tactics return result.ok == False with diagnostic messages:

>>> bad = state.try_tactic("exact rfl")
>>> bad.ok
False
>>> bad.messages
['type mismatch...']

Prograde tactics

Beyond try_tactic, structured proof construction is available:

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

Conv and calc modes

Enter conversion or calculation mode, then exit when done:

conv_state = state.conv_enter().state
# ... apply conv tactics ...
final_state = conv_state.fragment_exit().state

Goal state lifecycle

Goal states support serialisation, branching, and merging:

# Pickle to disk and restore later
state.pickle("/tmp/goal.bin")
restored = k.goal_unpickle("/tmp/goal.bin")

# Branch: apply different tactics to the same state
branch_a = state.try_tactic("intro n").state
branch_b = state.try_tactic("intros").state

# Continue: merge a branch back
merged = state.continue_with(branch_a)

# Resume with specific goal names
resumed = state.resume(["_uniq.42"])

Environment serialisation

The entire Lean environment can be saved and restored:

k.env_pickle("/tmp/env.bin")
k.env_unpickle("/tmp/env.bin")

Frontend processing

Process raw Lean source code against the current environment:

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

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

collect_sorrys extracts all sorry placeholders as goals — useful for AI-driven proof completion.

API reference

class lean_py.kernel.Kernel(lib: Any) → None

Bases: object

The kernel facade.

Wraps a LeanLibrary whose Lean source has imported LeanPy.Kernel and exposed the standard @[python] surface.

Example:

from lean_py import LeanLibrary
from lean_py.kernel import Kernel

lib = LeanLibrary.from_lake("path/to/project", "MyLib")
k = Kernel(lib)
k.init_search("")
k.load(["Init"])
s = k.goal_create("∀ n : Nat, n + 0 = n")
print(s.pretty())

decide(src: str) → str

Returns "true" / "false" / "<undecided>" / "<elab: ...>" etc.

Return type:

str

goal_create(type_str: str) → GoalState

Create a new goal state from a type expression string. Raises LeanError on parse / elaboration failure.

Return type:

GoalState

goal_unpickle(path: str) → GoalState

Load a goal state previously serialised with GoalState.pickle().

Return type:

GoalState

find_source_path(module_name: str) → str

Locate the .lean source file for module_name.

Return type:

str

process(source: str) → str

Process Lean source code against the current environment.

Returns a multi-line string of new constants per command, separated by \n---\n.

Return type:

str

collect_sorrys(source: str) → tuple[GoalState | None, str]

Extract all sorry placeholders in source as a draftable GoalState. Returns (state, message) — state is None if no sorries were found.

Return type:

tuple[GoalState | None, str]

class lean_py.kernel.GoalState(kernel: Kernel, handle: Any) → None

Bases: object

Opaque handle to a Lean GoalState. Methods dispatch back into the underlying Lean library.

try_have(binder_name: str, type_str: str) → TacticResult

Equivalent to have <binder_name> : <type_str> := ?.

Return type:

TacticResult

try_let(binder_name: str, type_str: str) → TacticResult

Equivalent to let <binder_name> : <type_str> := ?.

Return type:

TacticResult

try_define(binder_name: str, expr_str: str) → TacticResult

Equivalent to let <binder_name> := <expr_str>.

Return type:

TacticResult

try_draft(expr_str: str) → TacticResult

Substitute the goal with an expression that may contain sorrys, leaving the sorrys as fresh subgoals.

Return type:

TacticResult

diag() → str

Diagnostic dump of the GoalState’s internal mvar table.

Return type:

str

pickle(path: str) → None

Serialise the goal state to disk via Lean’s saveModuleData. Round-trips with Kernel.goal_unpickle(). Raises on error.

Return type:

None

replay(src: GoalState, src_prime: GoalState) → GoalState

Merge differential src → src_prime onto self (the dst).

Return type:

GoalState

subsume(goal_name: str, candidate_names: list[str]) → tuple[str, GoalState | None, str]

Try to discharge goal_name using one of candidate_names. Returns ("none"|"subsumed"|"cycle"|"error", optional new state, optional name of the candidate that subsumed).

Return type:

tuple[str, GoalState | None, str]

class lean_py.kernel.TacticResult(status: str, messages: list[str], state: GoalState | None) → None

Bases: object

Result of running a tactic.

status

one of "success", "failure", "parseError", "invalidAction".

messages

zero or more diagnostic / error messages.

state

the new GoalState if status == "success", else None.

classmethod parse(encoded: str, kernel: Kernel, raw_state: Any) → TacticResult

Parse the multi-line encoding produced by Lean’s encodeTacticResult.

Return type:

TacticResult