Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Getting Started with LeanLink
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
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]=
{id_proof,Vec.head,band_true,add_assoc_proof,comp_proof,even_two,Vec.ctorElimType,bor_false,zero_add_proof,bnot_bnot,Vec.cons,Vec,eq_transport,add_comm_proof,nat_eq_decide,contrapositive,Vec.nil,reverse_reverse,Vec.cons.elim,Vec.map,or_comm_proof,fin_example,exists_succ,sigma_example,add_zero_term,add_succ_term,Vec.nil.elim,modus_ponens,and_comm_proof,Vec.ctorElim,Vec.tail,Vec.ctorIdx}
Inspecting Types and Terms
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), 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} → Vec α (n + 1) → α
Expression Graphs
Expression Graphs
In[7]:=
env["modus_ponens"]["ExprGraph"]
Out[7]=
Constructing Expressions
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
| LeanTerm |
 | LeanApp |
 | LeanConst |
| LeanLitNat |
Out[8]=
LeanTerm
|
|
Its type, as Lean writes it:
In[9]:=
t["TypeForm"]
Out[9]=
Nat
In[10]:=
| LeanTerm |
| LeanForall |
| LeanConst |
| LeanConst |
Out[10]=
Type
Interactive Tactic Proofs
Interactive Tactic Proofs
In[11]:=
s0=
[env["id_proof"]]
| LeanState |
Out[11]=
1 goal | ||
|
Introduce the proposition:
In[12]:=
s1=
["intro P"][s0]
 | LeanTactic |
Out[12]=
1 goal | ||||
|
Then the hypothesis:
In[13]:=
s2=
["intro h"][s1]
| LeanTactic |
Out[13]=
1 goal | |||||
|
And close the goal with the hypothesis:
In[14]:=
s3=
["exact h"][s2]
| LeanTactic |
Out[14]=
✓ No goals
The proof is complete:
In[15]:=
s3["Complete"]
Out[15]=
True
Modus ponens: P(PQ)Q
Modus ponens:
P(PQ)Q
A whole proof as one tactic sequence:
In[16]:=
| LeanTactic |
| LeanState |
Out[16]=
True
Contrapositive: (PQ)(¬Q¬P)
Contrapositive:
(PQ)(¬Q¬P)
In[17]:=
| LeanTactic |
| LeanState |
Out[17]=
True
And commutativity: P∧QQ∧P
And commutativity:
P∧QQ∧P
In[18]:=
andComm=
[env["and_comm_proof"]]
| LeanState |
Out[18]=
1 goal | ||
|
constructor
In[19]:=
| LeanTactic |
| LeanTactic |
Out[19]=
2 goals | ||||||
| ||||||
|
Goal Properties
Goal Properties
Whether the proof is complete:
The Environment
The Environment
Exporting to Lean Source
Exporting to Lean Source
Importing from a Source String
Importing from a Source String
The theorem's statement:
Transpiling a Wolfram Proof
Transpiling a Wolfram Proof
Its constants:
The whole thing as Lean source:
Importing from Mathlib
Importing from Mathlib
Structured Tactics
Structured Tactics
Tactics can also be built structurally, with Lean-native names and Wolfram-valued arguments:
Applied the same way as string tactics, here to the identity's goal again:
Then the hypothesis:
And close the goal with it: