Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Checking Mathlib with TypeTheory
Checking Mathlib with TypeTheory
LeanLink loads a module of Mathlib straight from a built checkout, and imports its constants, each with every constant it depends on, into an environment of WolframInstitute/TypeTheory, a proof engine written in the Wolfram Language. TypeTheory's kernel checks every declaration again, independently of Lean's. This tutorial checks a whole module of Mathlib, , and shows what TypeTheory does not check yet.
Mathlib.Basic.Nonempty
Prerequisites
Prerequisites
The module comes from a built Mathlib checkout, as in the tutorial Exploring Mathlib with LeanLink, and the paclet must be installed:
WolframInstitute/TypeTheory
In[1]:=
mathlibDir=FileNameJoin[{$HomeDirectory,"src","mathlib4"}];mathlibReady=DirectoryQ[FileNameJoin[{mathlibDir,".lake","build"}]]
Out[1]=
True
Loading a Module
Loading a Module
Mathlib.Basic.Nonempty
In[2]:=
module="Mathlib.Basic.Nonempty";lean=IfmathlibReady,
[module,"ProjectDir"mathlibDir],
 | LeanImport |
Out[2]=
LeanEnvironment
| |||||
This object cannot be used as input. |
The module's own constants are those whose it is:
"Module"
In[3]:=
own=Select[Keys[lean],lean[#]["Module"]===module&];Length[own]
Out[3]=
37
They are theorems and definitions about , such as this one, which says that a statement about every proof that a type is inhabited is a statement about every element:
Nonempty
In[4]:=
lean["Nonempty.forall"]["TypeForm"]
Out[4]=
∀ {α : Sort u_3} {p : Nonempty α → Prop}, (∀ (h : Nonempty α), p h) ↔ ∀ (a : α), p ⋯
Checking It in TypeTheory
Checking It in TypeTheory
imports the 37 constants, and with them every constant they depend on, from Lean's core library and Mathlib's, into one environment, which TypeTheory's kernel checks declaration by declaration:
In[5]:=
checked=
[lean,own]
 | LeanToTypeTheory |
Out[5]=
TypeTheoryEnvironment
 |
|
What the environment holds, by kind; each inductive type comes with its constructors and the recursor TypeTheory generates for it, which the import compares with Lean's:
In[6]:=
Information[checked,"Kinds"]
Out[6]=
InductiveType19,Constructor21,Recursor19,Axiom2,Definition55,Theorem39
The module assumes two of Lean's axioms, and nothing else:
In[7]:=
Information[checked,"Axioms"]
Out[7]=
{propext,Classical.choice}
A Theorem in TypeTheory
A Theorem in TypeTheory
Lean names stay strings in TypeTheory. The statement of , as TypeTheory has checked it:
Nonempty.forall
In[8]:=
TypeTheoryCheck[TypeTheoryTerm["Nonempty.forall",checked]]
Out[8]=
∀
{α:Sortu_3}
∀
{p:Nonempty[α]→Prop}
∀
h:Nonempty[α]
∀
a:α
A definition shows its value, here the choice of an element from an instance of :
Nonempty
In[9]:=
checked["Classical.arbitrary"]
Out[9]=
definition | Classical.arbitrary | : | ∀ α:Sortu_3 ∀ [h:Nonempty[α]] |
In[10]:=
MakeBoxes["Iff"[a_,b_],form_]:=MakeBoxes[Equivalent[a,b],form];MakeBoxes["Eq"[a_,b_],form_]:=MakeBoxes[ab,form];MakeBoxes["Or"[a_,b_],form_]:=MakeBoxes[Or[a,b],form];TypeTheoryCheck[TypeTheoryTerm["Nonempty.forall",checked]]
Out[10]=
∀
{α:Sortu_3}
∀
{p:Nonempty[α]→Prop}
∀
h:Nonempty[α]
∀
a:α
Checking It Again
Checking It Again
The environment can be checked again from scratch: replays every declaration on an empty environment and compares what it gets with what is stored:
In[11]:=
TypeTheoryCheck[checked]
Out[11]=
Success
| ✓ |
|
Quotients
Quotients
Lean's kernel has quotient types built in: lifting a function to a quotient and applying it to a class gives the function's value. is proved with them. TypeTheory's kernel has the same quotient types, and the import declares Lean's as TypeTheory's own:
funext
In[12]:=
funext=
[lean,"funext"]
| LeanToTypeTheory |
Out[12]=
TypeTheoryEnvironment
|
|
The four constants come from one declaration, with Lean's names and Lean's equality:
In[13]:=
funext["Quot.lift"]
Out[13]=
TypeTheoryQuotients[Eq,{Quot,Quot.mk,Quot.lift,Quot.ind}]
The kernel computes with them, so the cone needs no rewrite rule:
In[14]:=
Information[funext,"RewriteRules"]
Out[14]=
{}
Lean's Prelude
Lean's Prelude
Lean's first file, , depends on 1,404 constants, and TypeTheory checks them all. Three things in it go beyond an inductive family of one type and a sum of literals, and the import follows Lean's kernel in each.
Init.Prelude
Lean's syntax trees are a nested inductive type: a node holds an array of trees. TypeTheory checks the nesting as Lean's kernel does, and generates a recursor on each container the trees are nested in, the array and the list inside it, which the import compares with Lean's and :
Lean.Syntax.rec_1
Lean.Syntax.rec_2
In[15]:=
syntax=
[lean,"Lean.Syntax"]
| LeanToTypeTheory |
Out[15]=
TypeTheoryEnvironment
|
|
The recursors of , one for the type and one for each container:
Lean.Syntax
In[16]:=
Select[Keys[syntax],MatchQ[InductiveRecursor["Lean.Syntax",___]]]
Out[16]=
{InductiveRecursor[Lean.Syntax],InductiveRecursor[Lean.Syntax,1],InductiveRecursor[Lean.Syntax,2]}
A string literal is the list of its characters, as Lean's kernel reads it, so the names of the syntax kinds import:
In[17]:=
kinds=
[lean,"Lean.nullKind"]
| LeanToTypeTheory |
Out[17]=
TypeTheoryEnvironment
|
|
The name of the null kind, a list of characters:
In[18]:=
kinds["Lean.nullKind"]
Out[18]=
definition | Lean.nullKind | : | Lean.SyntaxNodeKind:=Lean.Name.mkStr1[String.ofList[List.cons[Char.ofNat[110],List.cons[Char.ofNat[117],List.cons[Char.ofNat[108],List.cons[Char.ofNat[108],List.nil]]]]]] |
And Lean's kernel computes , , and the other operations on natural number literals with GMP. The import registers each with TypeTheory, which then computes it with integers, so a statement about the size of machine words, 2^32 or 2^64, checks at once:
Nat.add
Nat.mul
Nat.ble
In[19]:=
words=
[lean,"USize.size_eq"]
| LeanToTypeTheory |
Out[19]=
TypeTheoryEnvironment
|
|
The statement, checked:
In[20]:=
TypeTheoryCheck[TypeTheoryTerm["USize.size_eq",words]]
Out[20]=
USize.sizeOfNat.ofNat[4294967296]∨USize.sizeOfNat.ofNat[18446744073709551616]
Beyond the Prelude
Beyond the Prelude
LeanLink's repository has a script, , that imports every constant of a list of modules, with what it depends on in order, into one TypeTheory environment and reports what checks. The 25 modules at the bottom of Mathlib, from the logic of and unique existence to options, orderings and folds over lists, check completely, with all 5,361 constants they depend on, in about three and a half minutes. So do 117 modules higher up, each with every constant it depends on, among them the real and complex numbers, the exponential, logarithm and trigonometric functions, real powers, derivatives, polynomials, matrices and determinants, ideals, separable field extensions, Sylow's theorems, primes and factorizations, cardinals, simple graphs, measurable, metric, uniform and inner product spaces, normed fields, compactness and the p-adic numbers. checks too, with the 11,167 constants it depends on through Mathlib's construction of the real numbers, in about seven minutes.
typetheory_coverage.wls
Nonempty
Real.sqrt_nonneg
TypeTheory rejects none of these constants. Of the 71,203 distinct constants these modules and quadratic reciprocity depend on, six do not check within the five minutes the script allows each constant, and the 251 that depend on them are left unchecked: five proofs by that characters of and are 0 off the units, in the cone of quadratic reciprocity, and the associativity of multiplication in a tensor product of algebras. A proof that a tactic writes shares its subterms in Lean, and the import shares them too, reading and translating each distinct subterm once: a proof that writes in Lean's has 19 million nodes written out and 123 distinct ones, and a proof that writes in checks, with the 3,201 constants it depends on, in under two minutes.
decide
ZMod4
ZMod8
omega
Init.Data.Array.Extract
grind
Mathlib.Data.Int.Init
 |
|