Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Exploring Mathlib with LeanLink
Exploring Mathlib with LeanLink
is Lean's community mathematics library. LeanLink imports any built Mathlib module and lets you read theorem statements, dissect their binder structure, and inspect the typeclass machinery behind them - all from the Wolfram Language. Every example below is guarded so the page still builds where Mathlib is absent.
Prerequisites: Building Mathlib
Prerequisites: Building Mathlib
Install (the Lean version manager), then create a project with Mathlib as a dependency and build the modules used here:
elan
(* Terminal:
curl https://elan.lean-lang.org/install.sh | sh
mkdir -p ~/src/mathlib4 && cd ~/src/mathlib4
lake init MathlibTest math
lake exe cache get
lake build Mathlib.Algebra.Group.Basic
lake build Mathlib.Basic.Logic.Basic
*)
curl https://elan.lean-lang.org/install.sh | sh
mkdir -p ~/src/mathlib4 && cd ~/src/mathlib4
lake init MathlibTest math
lake exe cache get
lake build Mathlib.Algebra.Group.Basic
lake build Mathlib.Basic.Logic.Basic
*)
Point a variable at the checkout and record whether it is built:
In[1]:=
mathlibDir=FileNameJoin[{$HomeDirectory,"src","mathlib4"}];mathlibReady=DirectoryQ[FileNameJoin[{mathlibDir,".lake","build"}]]
Out[1]=
True
Loading a Module
Loading a Module
reads a module from the project. A keeps the result small - here, the constants whose names contain :
"Filter"
"mul"
In[2]:=
algEnv=IfmathlibReady,
["Mathlib.Algebra.Group.Basic","ProjectDir"mathlibDir,"Filter""mul"],"Mathlib not built"
 | LeanImport |
Out[2]=
LeanEnvironment
| |||||
This object cannot be used as input. |
Reading a Theorem's Type
Reading a Theorem's Type
A theorem's is the proposition it proves. states commutativity of multiplication:
"TypeForm"
mul_comm
In[3]:=
If[mathlibReady,algEnv["mul_comm"]["TypeForm"],"Mathlib not built"]
Out[3]=
∀ {G : Type u_1} [inst : CommMagma G] (a b : G), a * b = b * a
And - one is a left identity:
one_mul
In[4]:=
If[mathlibReady,algEnv["one_mul"]["TypeForm"],"Mathlib not built"]
Out[4]=
∀ {M : Type u_2} [inst : MulOneClass M] (a : M), 1 * a = a
Binder Annotations
Binder Annotations
Lean has three kinds of argument brackets:
◼
(x:T)
◼
{x:T}
◼
[inst:T]
In[5]:=
If[mathlibReady,algEnv["mul_comm"]["Parameters"]//Dataset,"Mathlib not built"]
Out[5]=
|
Reading it: to use you supply two explicit values and ; Lean infers the type and finds the instance automatically.
mul_comm
a
b
G
CommMagma
Typeclasses
Typeclasses
Typeclasses express algebraic structure. Selecting just the instance binders shows what demands of its type:
mul_comm
In[6]:=
If[mathlibReady,Select[algEnv["mul_comm"]["Parameters"],#Binder"instance"&]//Dataset,"Mathlib not built"]
Out[6]=
|
Propositional Logic
Propositional Logic
A different module, the same workflow. Load the logic basics, filtered to the commutativity lemmas:
In[7]:=
logicEnv=IfmathlibReady,
["Mathlib.Basic.Logic.Basic","ProjectDir"mathlibDir,"Filter""comm"],"Mathlib not built"
| LeanImport |
Out[7]=
LeanEnvironment
 |
|
And.comm
In[8]:=
If[mathlibReady,logicEnv["And.comm"]["TypeForm"],"Mathlib not built"]
Out[8]=
∀ {a b : Prop}, a ∧ b ↔ b ∧ a
And of disjunction, :
Or.comm
In[9]:=
If[mathlibReady,logicEnv["Or.comm"]["TypeForm"],"Mathlib not built"]
Out[9]=
∀ {a b : Prop}, a ∨ b ↔ b ∨ a
Expression Graphs
Expression Graphs
The full type of a theorem, drawn as its expression tree:
In[10]:=
If[mathlibReady,algEnv["mul_comm"]["ExprGraph"],"Mathlib not built"]
Out[10]=
Interactive Proofs
Interactive Proofs
Any imported theorem can be opened as a goal with and stepped with . Open and confirm it presents a single goal:
one_mul
In[11]:=
IfmathlibReady,
[algEnv,"one_mul"]["GoalCount"],"Mathlib not built"
| LeanState |
Out[11]=
1
 |
|
 |
|
""