Wolfram Language Paclet Repository

Community-contributed installable additions to the Wolfram Language

Wolfram/ LeanLink

(1.0.3) current version: 1.0.8 »

Native link between Wolfram Language and Lean 4

Contributed by: Nik Murzin

The entry points are LeanImport and LeanImportString (load an environment) and LeanExport / LeanExportString (write Lean source back). LeanTerm and LeanEnvironment are the two computable wrappers; the Parse*-style CIC heads - LeanConst, LeanApp, LeanForall, LeanLam, LeanLet, LeanBVar, LeanFVar, LeanSort, LeanLitNat, LeanLitStr, LeanProj - build expressions, with universe levels LeanLevelZero, LeanLevelSucc, LeanLevelMax. LeanState, LeanTactic, and LeanGoal run interactive proofs; ProofToLean transpiles a ProofObject; LeanCompile, LeanToFunction compile to native code; LeanExprGraph, LeanCallGraph, LeanListTheorems query a project out of process.

Installation Instructions

To install this paclet in your Wolfram Language environment, evaluate this code:
PacletInstall["Wolfram/LeanLink"]


To load the code after installation, evaluate this code:
Needs["Wolfram`LeanLink`"]

Details

LeanLink is a high-performance native bridge between the Wolfram Language and the Lean 4 theorem prover. It embeds the Lean runtime directly through a compiled LibraryLink shim - there is no subprocess per call and no text-protocol round-trip for the core API.
A loaded environment is a LeanEnvironment, a typed wrapper over Association[name → LeanTerm, …]. LeanImport loads constants from a compiled Lean module (Mathlib included); LeanImportString compiles a Lean source string on the fly.
Every Lean expression is a symbolic tree built from a small set of CIC heads - LeanConst, LeanApp, LeanForall, LeanLam, LeanBVar, LeanSort, LeanLitNat, … - each carrying box formatting so it displays in Lean-source notation.
A LeanTerm exposes "Type" / "Term" (expression trees), "TypeForm" / "TermForm" (pretty-printed source), "Parameters" (the unfolded binder chain), and "ExprGraph" / "CallGraph" (native Graph visualizations).
LeanState and LeanTactic drive interactive tactic proofs step by step; ProofToLean transpiles a Wolfram ProofObject into a checkable LeanEnvironment; LeanCompile and LeanToFunction lower a Lean definition to a FunctionCompile function.
The serialization backend is a compact binary (WXF) format, so goal states and expression trees cross the boundary without a parsing pass.

Examples

Basic Examples (4) 

Load the bundled example environment:

In[1]:=
env = LeanImport[ PacletObject["Wolfram/LeanLink"]["AssetLocation", "Examples"]]
Out[1]=

How many constants, and of what kinds:

In[2]:=
Length[env]
Out[2]=
In[3]:=
Information[env, "Kinds"]
Out[3]=

A single constant is a LeanTerm summary box:

In[4]:=
env["id_proof"]
Out[4]=

Its type, pretty-printed as Lean source - the proposition it proves:

In[5]:=
env["id_proof"]["TypeForm"]
Out[5]=

And the proof term:

In[6]:=
env["id_proof"]["TermForm"]
Out[6]=

Every expression is a tree; "ExprGraph" draws it:

In[7]:=
env["id_proof"]["ExprGraph"]
Out[7]=

"CallGraph" shows which constants a proof depends on:

In[8]:=
env["or_comm_proof"]["CallGraph"]
Out[8]=

Scope (2) 

Import from Mathlib by pointing "ProjectDir" at a built mathlib4 checkout (gated so the page still builds without one):

In[9]:=
mathlibDir = FileNameJoin[{$HomeDirectory, "src", "mathlib4"}]; If[ DirectoryQ[FileNameJoin[{mathlibDir, ".lake", "build"}]], mulComm = LeanImport["Mathlib.Algebra.Group.Basic", "ProjectDir" -> mathlibDir, "Filter" -> "mul_comm"]; mulComm["mul_comm"]["TypeForm"], "Mathlib not built - run: lake exe cache get && lake build Mathlib.Algebra.Group.Basic" ]
Out[9]=

The "Parameters" property unfolds a theorem's binder chain - explicit, implicit, and instance arguments - as a Dataset:

In[10]:=
env["modus_ponens"]["Parameters"] // Dataset
Out[10]=

Applications (3) 

Open any theorem as a proof goal and step through it with tactics:

In[11]:=
s0 = LeanState[env["id_proof"]]
Out[11]=
In[12]:=
s1 = LeanTactic[{"intro P", "intro h", "exact h"}][s0]; s1["Complete"]
Out[12]=

Transpile a Wolfram ProofObject into a checkable Lean environment:

In[13]:=
leanEnv = ProofToLean[FindEquationalProof[a == c, {a == b, b == c}]]; Keys[leanEnv]
Out[13]=
In[14]:=
LeanState[leanEnv["FinalGoal"]]["Complete"]
Out[14]=

Lower a (non-dependent) Lean definition to native code via FunctionCompile:

In[15]:=
addEnv = LeanImportString["def myAdd (x y : Nat) : Nat := x + y"]; cf = LeanCompile[addEnv["myAdd"]]; cf[3, 4]
Out[15]=

Properties and Relations (1) 

LeanImportString round-trips with LeanExportString: import a source string, query it, and export an environment back to Lean source:

In[16]:=
imported = LeanImportString["theorem myT : Nat.succ 0 = 1 := rfl"]; imported["myT"]["TypeForm"]
Out[16]=

ProofToLean complements MetamathImport - both bring an external formal-proof corpus into the Wolfram Language; LeanLink targets Lean 4 / Mathlib and additionally drives the prover interactively.

Possible Issues

The native bridge needs the platform dylib under LeanLink/LibraryResources/. Mathlib import and the out-of-process graph functions (LeanExprGraph, LeanCallGraph) additionally need elan / lake on PATH and a built project - LeanImport of an unbuilt module returns an empty environment.
LeanCompile's dependent-type path (Vector-sized signatures via TypePi) requires a forked Wolfram compiler; the non-dependent path works against the stock compiler.
A type shown in isolation can print an unresolved bound variable as #0 / #1; the full-theorem "TypeForm" resolves binder names.

Neat Examples (1) 

The type of a Mathlib theorem, drawn as its expression tree (gated on a built checkout):

In[17]:=
If[ DirectoryQ[ FileNameJoin[{$HomeDirectory, "src", "mathlib4", ".lake", "build"}]], LeanImport["Mathlib.Logic.Basic", "ProjectDir" -> FileNameJoin[{$HomeDirectory, "src", "mathlib4"}], "Filter" -> "And.comm"]["And.comm"]["ExprGraph"], "Mathlib not built" ]
Out[17]=

Disclosures

Compatibility

Wolfram Language Version 14.0

Version History

  • 1.0.8 – 10 August 2026
  • 1.0.7 – 08 August 2026
  • 1.0.6 – 28 June 2026
  • 1.0.5 – 27 June 2026
  • 1.0.4 – 06 June 2026
  • 1.0.3 – 06 June 2026
  • 1.0.2 – 01 April 2026
  • 1.0.1 – 31 March 2026
  • 1.0.0 – 31 March 2026

License Information

MIT License

Paclet Source

Source Metadata

  • Citation:
    • Leonardo de Moura, Sebastian Ullrich, *The Lean 4 Theorem Prover and Programming Language*, CADE 28, 2021

See Also