Formalized Math Systems

LEAN [ mathlib ]

https://leanprover-community.github.io/papers/mathlib-paper.pdf

Dependency graph

In[]:=
(*takesabout20sectoevaluate*)​​vertexNameAssociation=Uncompress@
vertex association
;​​indexedEdges=Uncompress@
edges
;​​mathlib=Graph[indexedEdges/.vertexNameAssociation]
Out[]=
Graph
Vertex count: 107229
Edge count: 2151553


Documentation strings

Documentation strings are still fairly rare in mathlib, but there are about 12000 here:
In[]:=
docs=Uncompress
documentation association
;
In[]:=
Take[docs,5]
Out[]=
tangent_bundle_proj_openThe tangent bundle projection on the basis is an open map.,partial_orderA partial order is a reflexive, transitive, antisymmetric relation `≤`.,expr.is_sortTests whether an expression is a sort.,environmentAn __environment__ contains all of the declarations and notation that have been defined so far.,times_cont_diff.differentiableIf a function is `C^n` with `n ≥ 1`, then it is differentiable.

Examples

In[]:=
indexedEdges//ByteCount
Out[]=
206549168
In[]:=
AcyclicGraphQ[mathlib]
Out[]=
True
In[]:=
leantheorems=Values[vertexNameAssociation];​​RandomSample[leantheorems,12]
Out[]=
{complex.cos_pi_div_two,enorm.mk,function.support_inv,asymptotics.is_o.is_O,measure_theory.measure.complete_lattice,reader_t.monad_run.equations._eqn_1,smt_tactic.interactive.trace_state,submodule.mem_div_iff_smul_subset,list.head'_map,tactic.unify,ulift.ring_equiv._proof_1,prime_spectrum.mem_vanishing_ideal}
In[]:=
WeaklyConnectedComponents[mathlib]//Length
Out[]=
1
In[]:=
Histogram[VertexDegree[mathlib],{"Log",60}]
Out[]=
In[]:=
Take[Reverse[Sort[{VertexInDegree[mathlib,#],#}&/@theorems]],12]
Out[]=
{{67608,eq},{39097,eq.refl},{22575,id},{21048,nat},{20101,eq.mpr},{17039,has_zero.zero},{15636,set},{14909,has_mem.mem},{14773,congr_arg},{14677,has_add.add},{14613,eq.rec},{14157,has_one.one}}
In[]:=
Take[Reverse[Sort[{VertexOutDegree[mathlib,#],#}&/@theorems]],12]
Out[]=
{{361,measure_theory.hahn_decomposition},{337,formal_multilinear_series.comp_summable_nnreal},{326,Gromov_Hausdorff.totally_bounded},{299,measure_theory.simple_func_sequence_tendsto},{293,primorial_le_4_pow},{292,_private.3105277429.prime_sum_four_squares},{292,exists_norm_eq_infi_of_complete_convex},{289,real.sin_bound},{286,real.abs_log_sub_add_sum_range_le},{282,pythagorean_triple.is_primitive_classified_of_coprime_of_odd_of_pos},{279,complex.exists_root},{276,real.cos_bound}}
In[]:=
{VertexEccentricity[mathlib,#[[2]]],#[[2]]}&/@%
Out[]=
{{34,measure_theory.hahn_decomposition},{25,formal_multilinear_series.comp_summable_nnreal},{23,Gromov_Hausdorff.totally_bounded},{21,measure_theory.simple_func_sequence_tendsto},{17,primorial_le_4_pow},{20,_private.3105277429.prime_sum_four_squares},{23,exists_norm_eq_infi_of_complete_convex},{18,real.sin_bound},{22,real.abs_log_sub_add_sum_range_le},{18,pythagorean_triple.is_primitive_classified_of_coprime_of_odd_of_pos},{35,complex.exists_root},{18,real.cos_bound}}
In[]:=
Dataset@DeleteMissing@AssociationMap[docs,%[[All,2]]]
Out[]=
In[]:=
Take[Reverse[Sort[Transpose[{PageRankCentrality[mathlib,0.1],theorems}]]],12]
Out[]=
{{0.00444062,eq},{0.00190044,eq.refl},{0.00143555,nat},{0.000870155,set},{0.00081753,list},{0.000757398,id},{0.000692828,category_theory.category},{0.000676603,has_zero.zero},{0.000642475,has_add.add},{0.000638713,has_mem.mem},{0.000614914,id_rhs},{0.000592634,has_one.one}}

LEAN exploration

In[]:=
VertexCount[mathlib]
Out[]=
107229
In[]:=
Take[vertexNameAssociation,10]
Out[]=
1cau_seq.has_mul._proof_1,2preorder.to_has_lt,3differentiable_at.smul_const,4mul_action.to_has_scalar,5tendsto_multiset_sum,6multiset.sum,7neg_of_mul_pos_right,8linear_order.to_partial_order,9nat.bit_lt_bit_iff,10decidable_linear_ordered_semiring.to_linear_ordered_semiring
In[]:=
Count[VertexInDegree[mathlib],0]
Out[]=
31905
In[]:=
Count[VertexOutDegree[mathlib],0]
Out[]=
586
In[]:=
Extract[VertexList[mathlib],Position[VertexOutDegree[mathlib],0]]
In[]:=
Take[theorems,5]
Out[]=
{cau_seq.has_mul._proof_1,preorder.to_has_lt,differentiable_at.smul_const,mul_action.to_has_scalar,tendsto_multiset_sum}

Metadata

In[]:=
mathlibKinds=Uncompress@
kinds
;
In[]:=
mathlibMeta=Uncompress@
meta
;
In[]:=
Take[mathlibKinds,20]
Out[]=
group.exists_list_of_mem_closurethm,lt_add_onethm,differentiable_at.smul_constthm,tangent_bundle_proj_openthm,partial_ordercnst,tactic.ring_exp.mul_pp_pf_overlapthm,eq_ff_of_not_eq_ttthm,expr.is_sortdef,environmentcnst,equiv.of_injective_applythm,times_cont_diff.differentiablethm,nat.elim_zerothm,simple_graph.adj_iff_exists_edgethm,int.lt_of_le_sub_onethm,multiset.card_eq_zerothm,topological_space.first_countable_topologycnst,filter.eventually_botthm,pow_eq_zerothm,tactic.mk_congr_argcnst,valuation.self_le_supp_comapthm
In[]:=
Counts[mathlibKinds]
Out[]=
thm35690,cnst1592,def15733,ax1
In[]:=
Take[mathlibMeta,20]
Out[]=
group.exists_list_of_mem_closureFalse,lt_add_oneFalse,differentiable_at.smul_constFalse,tangent_bundle_proj_openFalse,partial_orderFalse,tactic.ring_exp.mul_pp_pf_overlapFalse,eq_ff_of_not_eq_ttFalse,expr.is_sortTrue,environmentTrue,equiv.of_injective_applyFalse,times_cont_diff.differentiableFalse,nat.elim_zeroFalse,simple_graph.adj_iff_exists_edgeFalse,int.lt_of_le_sub_oneFalse,multiset.card_eq_zeroFalse,topological_space.first_countable_topologyFalse,filter.eventually_botFalse,pow_eq_zeroFalse,tactic.mk_congr_argTrue,valuation.self_le_supp_comapFalse
In[]:=
Counts[mathlibMeta]
Out[]=
False49440,True3576
In[]:=
thmnames=Keys[Select[mathlibKinds,#==="thm"&]];

Pythagorean theorem

Pythagorean theorem:
[[[[ Try transitive reduction ]]]]

Euclid version

Dimensions

Metamath

http://us.metamath.org/mpeuni/2p2e4.html

Exploration

Pythag

Mizar

Reading Mizar files

Setup

All files

Theorems

There are theorem texts of the form:
All others
Histogram of string lengths:

SW Explorations