LeanLink — Interactive Lean from Wolfram Language

Setup
(*PacletDirectoryLoad[NotebookDirectory[]//ParentDirectory];*)​​PacletInstall["https://www.wolframcloud.com/obj/nikm/LeanLink.paclet",ForceVersionInstall->True];
Get["LeanLink`"];
Importing a Lean Environment
Load the bundled Examples file:
env=LeanImportString[​​Import[PacletObject["LeanLink"]["AssetLocation","Examples"],"Text"]]
Out[]=
LeanEnvironment
Constants: 25
Kinds: 6 def18 theorem1 inductive

Keys[env]
Out[]=
{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
env["id_proof"]["TypeForm"]
Out[]=
∀ (P : Prop) (a : P), P
env["id_proof"]["Type"]
Out[]=
(P:Prop)(a:
#0
)
#1
env["Vec.head"]["TypeForm",1]
Out[]=
∀ {α : Type} {n : Nat} (a : Vec α instHAdd Nat instAddNat.0 n 1), α
Expression Graphs
env["modus_ponens"]["ExprGraph"]
Out[]=
Constructing Expressions
Build a Lean expression and bind it to an environment for type-checking:
t=LeanTerm[LeanApp[LeanConst["Nat.succ"],LeanLitNat[42]],env]
Out[]=
LeanTerm
Kind: expr
Name: user_expr

t["TypeForm"]
Out[]=
Nat
Type-check a forall expression:
LeanTerm[LeanForall["n",LeanConst["Nat"],LeanConst["Nat"],"default"],env]["Type"]
Out[]=
Type
Interactive Tactic Proofs

Identity:
∀P:Prop,PP

s0=LeanState[env["id_proof"]]
Out[]=
1 goal
————————————
⊳ ∀ (P : Prop) (a : P), P
s1=LeanTactic["intro P"][s0]
Out[]=
1 goal
P : Prop
————————————
⊳ ∀ (a : _fvar), _fvar
s2=LeanTactic["intro h"][s1]
Out[]=
1 goal
P : Prop
h : _fvar
————————————
⊳ _fvar
s3=LeanTactic["exact h"][s2]
Out[]=
✓ No goals

Modus Ponens:
P(PQ)Q

s0=LeanState[env["modus_ponens"]]
Out[]=
1 goal
————————————
⊳ ∀ (P : Prop) (Q : Prop) (a : P) (a : ∀ (a : P), Q), Q
LeanTactic[{"intro P Q hP hPQ","exact hPQ hP"}][s0]
Out[]=
✓ No goals

Contrapositive:
(PQ)(¬Q¬P)

s0=LeanState[env["contrapositive"]]
Out[]=
1 goal
————————————
⊳ ∀ (P : Prop) (Q : Prop) (a : ∀ (a : P), Q) (a : ¬Q), ¬P
LeanTactic[{"intro P Q hPQ hnQ hP","apply hnQ","exact hPQ hP"}][s0]
Out[]=
✓ No goals

And Commutativity:
P⋀QQ⋀P

s0=LeanState[env["and_comm_proof"]]
Out[]=
1 goal
————————————
⊳ ∀ (P : Prop) (Q : Prop) (a : P ∧ Q), Q ∧ P
s1=LeanTactic["intro P Q h"][s0]
Out[]=
1 goal
P : Prop
Q : Prop
h : _fvar ∧ _fvar
————————————
⊳ _fvar ∧ _fvar
s2=LeanTactic["constructor"][s1]
Out[]=
2 goals
P : Prop
Q : Prop
h : _fvar ∧ _fvar
————————————
⊳ ?_
P : Prop
Q : Prop
h : _fvar ∧ _fvar
————————————
⊳ ?_

Accessing Goal Properties

s0=LeanState[env["id_proof"]];​​s0["Goals"]
Out[]=

————————————
⊳ ∀ (P : Prop) (a : P), P

s0["Goals"][[1]]["Target"]
Out[]=
∀ (P : Prop), P → P
s0["Goals"][[1]]["Context"]
Out[]=
{}
LeanEnvironment
Exporting to Source

Single term

Full environment to file

Importing from Source String
ProofToLean — ProofObject to Lean

Inspecting the result

Generated Lean source

Roundtrip: ProofObject → LeanTerm → Source → LeanImportString

Auto-completing proofs with LeanState

Importing from Mathlib
Structured Tactics
Tactics are symbolic objects with Lean-native names:
Apply structured tactics to proof states: