LeanLink — Exploring Mathlib
LeanLink — Exploring Mathlib
Prerequisites: Installing Mathlib
Install elan (Lean version manager) if not already installed:
(* Terminal: curl https://elan.lean-lang.org/install.sh | sh *)
Create a Lean project with Mathlib as a dependency and build the modules used in this notebook:
(* Terminal:
mkdir -p ~/src/mathlib4 && cd ~/src/mathlib4
lake init MathlibTest math
lake exe cache get
lake build Mathlib.Tactic.Ring
lake build Mathlib.Algebra.Group.Basic
lake build Mathlib.Logic.Basic
lake build Mathlib.FieldTheory.IsAlgClosed.Basic
*)
mkdir -p ~/src/mathlib4 && cd ~/src/mathlib4
lake init MathlibTest math
lake exe cache get
lake build Mathlib.Tactic.Ring
lake build Mathlib.Algebra.Group.Basic
lake build Mathlib.Logic.Basic
lake build Mathlib.FieldTheory.IsAlgClosed.Basic
*)
Setup
(*PacletDirectoryLoad[NotebookDirectory[]//ParentDirectory];*)PacletInstall["https://www.wolframcloud.com/obj/nikm/LeanLink.paclet",ForceVersionInstall->True]
Out[]=
PacletObject
Get["LeanLink`"];mathlibDir=FileNameJoin[{$HomeDirectory,"src","mathlib4"}];
Part 1: Types and Propositions
In Lean 4 (and Mathlib), every expression has a type. Propositions live in , data types live in . LeanLink lets us inspect these directly.
Prop
Type u
Loading an environment
Loading an environment
algEnv=LeanImport["Mathlib.Algebra.Group.Basic","ProjectDir"->mathlibDir]
Out[]=
LeanEnvironment
Length[algEnv]
Out[]=
115060
Reading a theorem's type
Reading a theorem's type
mul_comm
algEnv["mul_comm"]["TypeForm"]
Out[]=
∀ {G : Type u_1} [inst : CommMagma G] (a : G) (b : G), a * b = b * a
Compare with — adding zero on the right:
add_zero
algEnv["add_zero"]["TypeForm"]
Out[]=
∀ {M : Type u} [inst : AddZeroClass M] (a : M), a + 0 = a
And — multiplying by one on the left:
one_mul
algEnv["one_mul"]["TypeForm"]
Out[]=
∀ {M : Type u} [inst : MulOneClass M] (a : M), 1 * a = a
The expression tree
The expression tree
Behind the pretty-printed string is a symbolic expression tree. returns it:
"Type"
algEnv["mul_comm"]["Type"]
Out[]=
{G:Sortu_1+1}[inst:](a:)(b:)
CommMagma
#0
#1
#2
Eq
#3
HMul.hMul
#3
#3
#3
instHMul
#3
CommMagma.toMul
#3
#2
#1
#0
HMul.hMul
#3
#3
#3
instHMul
#3
CommMagma.toMul
#3
#2
#0
#1
Every Lean expression is built from a small set of constructors: (named constant), (function application), (universal quantifier / function type), (bound variable), , and .
LeanConst
LeanApp
LeanForall
LeanBVar
LeanLambda
LeanSort
Part 2: Understanding Binder Annotations
Lean uses three kinds of argument brackets:
◼
(x : T)
◼
{x : T}
◼
[inst : T]
The new property peels apart the forall chain and shows each argument:
"Parameters"
algEnv["mul_comm"]["Parameters"]//Dataset
Out[]=
The output tells us: to use , we provide two explicit values and , and Lean auto-resolves the type (implicit) and the instance.
mul_comm
a
b
G
CommMagma
Comparing parameter structures
Comparing parameter structures
algEnv["add_zero"]["Parameters"]//Dataset
Out[]=
add_zero
AddZeroClass
Nat
Int
Real
algEnv["neg_add_cancel"]["Parameters"]//Dataset
Out[]=
neg_add_cancel
AddGroup
Part 3: Typeclasses
Typeclasses are Lean's way of expressing algebraic structure. When you see , Lean automatically searches for a proof that is a field.
[inst : Field k]
k
What typeclasses does mul_comm need?
What typeclasses does need?
mul_comm
Select[algEnv["mul_comm"]["Parameters"],#Binder=="instance"&]//Dataset
Out[]=
What typeclasses does sub_eq_add_neg need?
What typeclasses does need?
sub_eq_add_neg
algEnv["sub_eq_add_neg"]["Parameters"]//Dataset
Out[]=
Building a typeclass hierarchy
Building a typeclass hierarchy
Each typeclass extends others. An extends extends . We can see this by inspecting the type of the typeclass itself:
AddGroup
AddMonoid
AddZeroClass
algEnv["AddGroup"]["TypeForm"]
Out[]=
∀ (A : Type u), Type u
Part 4: Propositional Logic
logicEnv=LeanImport["Mathlib.Logic.Basic","ProjectDir"->mathlibDir]
Out[]=
LeanEnvironment
The law of excluded middle
The law of excluded middle
Every proposition is either true or false:
logicEnv["Classical.em"]["TypeForm"]
Out[]=
∀ (p : Prop), p ∨ ¬p
logicEnv["Classical.em"]["Parameters"]//Dataset
Out[]=
Commutativity of connectives
Commutativity of connectives
Double negation
Double negation
Part 5: Interactive Proofs
LeanLink can open any theorem as a proof goal and let you step through it with tactics.
Opening a proof goal
Opening a proof goal
Applying tactics
Applying tactics
Introduce the universally quantified variables:
Part 6: The Fundamental Theorem of Algebra
All IsAlgClosed theorems
All IsAlgClosed theorems
The core theorem: existence of roots
The core theorem: existence of roots
Dissecting the FTA parameters
Dissecting the FTA parameters
Reading the parameter table:
The conclusion
The conclusion
After all the parameters, the return type (the thing being proved) is:
Every polynomial splits
Every polynomial splits
A stronger form: every polynomial factors completely over an algebraically closed field:
Consequences
Consequences
N-th roots exist in algebraically closed fields:
Square roots exist:
Algebraically closed fields are necessarily infinite:
The construction of the typeclass
The construction of the typeclass
Expression tree of the FTA
Expression tree of the FTA
Open the proof goal:
The state shows the goal we need to prove. Not yet complete:
Introduce the variables:
Close it with the axiom: