Formalized Math Systems
Formalized Math Systems
LEAN [ mathlib ]
LEAN [ mathlib ]
Dependency graph
Dependency graph
In[]:=
(*takesabout20sectoevaluate*)vertexNameAssociation=Uncompress@;indexedEdges=Uncompress@;mathlib=Graph[indexedEdges/.vertexNameAssociation]
Out[]=
Graph
Documentation strings
Documentation strings
Documentation strings are still fairly rare in mathlib, but there are about 12000 here:
In[]:=
docs=Uncompress;
In[]:=
Take[docs,5]
Out[]=
tangent_bundle_proj_openThe tangent bundle projection on the basis is an open map.,partial_orderA partial order is a reflexive, transitive, antisymmetric relation `≤`.,expr.is_sortTests whether an expression is a sort.,environmentAn __environment__ contains all of the declarations and notation that have been defined so far.,times_cont_diff.differentiableIf a function is `C^n` with `n ≥ 1`, then it is differentiable.
Examples
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
LEAN exploration
In[]:=
VertexCount[mathlib]
Out[]=
107229
In[]:=
Take[vertexNameAssociation,10]
Out[]=
1cau_seq.has_mul._proof_1,2preorder.to_has_lt,3differentiable_at.smul_const,4mul_action.to_has_scalar,5tendsto_multiset_sum,6multiset.sum,7neg_of_mul_pos_right,8linear_order.to_partial_order,9nat.bit_lt_bit_iff,10decidable_linear_ordered_semiring.to_linear_ordered_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
Metadata
In[]:=
mathlibKinds=Uncompress@;
In[]:=
mathlibMeta=Uncompress@;
In[]:=
Take[mathlibKinds,20]
Out[]=
group.exists_list_of_mem_closurethm,lt_add_onethm,differentiable_at.smul_constthm,tangent_bundle_proj_openthm,partial_ordercnst,tactic.ring_exp.mul_pp_pf_overlapthm,eq_ff_of_not_eq_ttthm,expr.is_sortdef,environmentcnst,equiv.of_injective_applythm,times_cont_diff.differentiablethm,nat.elim_zerothm,simple_graph.adj_iff_exists_edgethm,int.lt_of_le_sub_onethm,multiset.card_eq_zerothm,topological_space.first_countable_topologycnst,filter.eventually_botthm,pow_eq_zerothm,tactic.mk_congr_argcnst,valuation.self_le_supp_comapthm
In[]:=
Counts[mathlibKinds]
Out[]=
thm35690,cnst1592,def15733,ax1
In[]:=
Take[mathlibMeta,20]
Out[]=
group.exists_list_of_mem_closureFalse,lt_add_oneFalse,differentiable_at.smul_constFalse,tangent_bundle_proj_openFalse,partial_orderFalse,tactic.ring_exp.mul_pp_pf_overlapFalse,eq_ff_of_not_eq_ttFalse,expr.is_sortTrue,environmentTrue,equiv.of_injective_applyFalse,times_cont_diff.differentiableFalse,nat.elim_zeroFalse,simple_graph.adj_iff_exists_edgeFalse,int.lt_of_le_sub_oneFalse,multiset.card_eq_zeroFalse,topological_space.first_countable_topologyFalse,filter.eventually_botFalse,pow_eq_zeroFalse,tactic.mk_congr_argTrue,valuation.self_le_supp_comapFalse
In[]:=
Counts[mathlibMeta]
Out[]=
False49440,True3576
In[]:=
thmnames=Keys[Select[mathlibKinds,#==="thm"&]];
Pythagorean theorem
Pythagorean theorem
Pythagorean theorem:
[[[[ Try transitive reduction ]]]]
Euclid version
Euclid version
Dimensions
Dimensions
Metamath
Metamath
Exploration
Exploration
Pythag
Pythag
Mizar
Mizar
Reading Mizar files
Reading Mizar files
Setup
Setup
All files
All files
Theorems
Theorems
There are theorem texts of the form:
All others
Histogram of string lengths:
SW Explorations
SW Explorations