Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Getting Started with LeanLink
LeanLink embeds the theorem prover in the Wolfram Language. This tutorial loads a small bundled environment, inspects Lean types and proof terms, runs interactive tactic proofs, and round-trips proofs between the two systems. One environment is imported up front and reused throughout.
Importing a Lean Environment
loads the constants of a compiled Lean module or file into a . Here we load the example file bundled with the paclet:
.lean
In[1]:=
env=
[PacletObject["Wolfram/LeanLink"]["AssetLocation","Examples"]]
 | LeanImport |
Out[1]=
LeanEnvironment
 |
|
It holds a handful of definitions and proofs:
In[2]:=
Keys[env]
Out[2]=
{Vec.head,id_proof,add_zero_term,fin_example,add_comm_proof,contrapositive,bor_false,eq_transport,add_succ_term,Vec.map,sigma_example,bnot_bnot,even_two,exists_succ,Vec.tail,and_comm_proof,add_assoc_proof,Vec,band_true,comp_proof,reverse_reverse,modus_ponens,nat_eq_decide,zero_add_proof,or_comm_proof}
Inspecting Types and Terms
Index the environment by name to get a . Its is the proposition it proves (or the type it inhabits), pretty-printed as Lean source:
"TypeForm"
In[3]:=
env["id_proof"]["TypeForm"]
Out[3]=
∀ (P : Prop) (a : P), P
The is the proof term itself:
"TermForm"
In[4]:=
env["id_proof"]["TermForm"]
Out[4]=
fun x hp => hp
Behind the pretty-print is a symbolic expression tree, built from the CIC heads , , , , and friends. The property returns it:
"Type"
In[5]:=
env["id_proof"]["Type"]
Out[5]=
(P:Prop)(a:)
#0
#1
A dependent type from the same file - the head of a length-indexed vector:
In[6]:=
env["Vec.head"]["TypeForm"]
Out[6]=
∀ {α : Type} {n : Nat} (a : Vec α n + 1), α
Expression Graphs
In[7]:=
env["modus_ponens"]["ExprGraph"]
Out[7]=
Constructing Expressions
You can build a Lean expression from the CIC heads and bind it to an environment for type-checking with . Applying to a literal:
Nat.succ
In[8]:=
t=
["Nat.succ"],
[42],env;t["TypeForm"]
 | LeanTerm |
 | LeanApp |
 | LeanConst |
| LeanLitNat |
Out[8]=
Nat
In[9]:=
| LeanTerm |
 | LeanForall |
| LeanConst |
| LeanConst |
Out[9]=
Type
Interactive Tactic Proofs
In[10]:=
s0=
[env["id_proof"]]
| LeanState |
Out[10]=
1 goal | ||
|
Introduce the proposition and hypothesis, then close with the hypothesis:
In[11]:=
s1=
["intro P"][s0];s2=
["intro h"][s1];s3=
["exact h"][s2];s3["Complete"]
| LeanTactic |
| LeanTactic |
| LeanTactic |
Out[11]=
True
Modus ponens: P(PQ)Q
Modus ponens:
P(PQ)Q
A whole proof as one tactic sequence:
In[12]:=
| LeanTactic |
| LeanState |
Out[12]=
True
Contrapositive: (PQ)(¬Q¬P)
Contrapositive:
(PQ)(¬Q¬P)
In[13]:=
| LeanTactic |
| LeanState |
Out[13]=
True
And commutativity: P⋀QQ⋀P
And commutativity:
P⋀QQ⋀P
constructor
In[14]:=
s0=
[env["and_comm_proof"]];
["constructor"]
["intro P Q h"][s0]["GoalCount"]
| LeanState |
| LeanTactic |
| LeanTactic |
Out[14]=
2
Goal Properties
In[15]:=
s0=
[env["id_proof"]];s0["Goals"]〚1〛["Target"]
| LeanState |
Out[15]=
∀ (P : Prop), P → P
In[16]:=
s0["Complete"]
Out[16]=
False
The Environment
In[17]:=
Information[env,"Kinds"]
Out[17]=
def6,theorem18,inductive1
Exporting to Lean Source
renders a constant's type back as Lean source (bound variables in a bare type print as de Bruijn indices , ):
#0
#1
In[18]:=
 | LeanExportString |
Out[18]=
∀ (P : Prop) (a : #0), #1
Importing from a Source String
compiles Lean source on the fly:
In[19]:=
imported=
["theorem myT : Nat.succ 0 = 1 := rfl"];imported["myT"]["TypeForm"]
| LeanImportString |
Out[19]=
Nat.succ 0 = 1
Transpiling a Wolfram Proof
The whole thing as Lean source:
Importing from Mathlib
Structured Tactics
Tactics can also be built structurally, with Lean-native names and Wolfram-valued arguments:
Applied the same way as string tactics: