Wolfram Language Paclet Repository

Community-contributed installable additions to the Wolfram Language

Wolfram/ LeanLink

Native link between Wolfram Language and Lean 4

Contributed by: Nik Murzin

LeanLink is a high-performance native bridge between the Wolfram Language and the Lean 4 theorem prover. It enables interoperability, allowing users to import entire Lean projects like Mathlib directly into a native Wolfram environment. Utilizing a fast binary serialization backend, the package lets you seamlessly visualize proof dependencies as native graphs, transpile mathematical proofs into validated Lean code, and compile formal Lean types into executable Wolfram functions.

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`"]

Examples

Basic Examples (3) 

Load an example lean environment:

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

Query its properties:

In[2]:=
Information[env, "Properties"]
Out[2]=
In[3]:=
Information[env, "Constants"]
Out[3]=

Inspect Lean terms:

In[4]:=
env["id_proof"]
Out[4]=
In[5]:=
env["id_proof"]["Properties"]
Out[5]=
In[6]:=
env["id_proof"]["TypeForm"]
Out[6]=
In[7]:=
env["id_proof"]["TermForm"]
Out[7]=
In[8]:=
env["id_proof"]["ExprGraph"]
Out[8]=
In[9]:=
env["or_comm_proof"]["CallGraph"]
Out[9]=

Scope (3) 

Load mathlib environment:

In[10]:=
mathlib = LeanImport["Mathlib.Algebra.Group.Basic", "ProjectDir" -> FileNameJoin[{$HomeDirectory, "src", "mathlib4"}]]
Out[10]=
In[11]:=
mathlib["mul_comm"]
Out[11]=

Create Lean state for interactive proving:

In[12]:=
s = LeanState[mathlib, "add_zero"]
Out[12]=

Apply tactic:

In[13]:=
s /= LeanTactic["intro", {"M", "inst", "a"}]
Out[13]=

Disclosures

  • Wolfram Language built-in symbols
  • Local system interactions
  • Learn More »

Compatibility

Wolfram Language Version 14.0

Version History

  • 1.0.2 – 01 April 2026
  • 1.0.1 – 31 March 2026
  • 1.0.0 – 31 March 2026

License Information

MIT License

Paclet Source

See Also