Topic: 50000 theorems in mathlib
Kevin Buzzard (Mar 18 2021 at 17:08):
Right now we have 49993 theorems in mathlib according to https://leanprover-community.github.io/mathlib_stats.html . I don't really know what they're counting and I'm very surprised that we only have twice as many theorems as definitions, but I guess tomorrow it will go past 50,000.
Floris van Doorn (Mar 19 2021 at 19:12):
One part of the large number of definitions is that instances are counted towards the definitions, and instances are about 1/3 of definitions:
-- after running `scripts/mk_all.sh` import all open tactic run_cmd do e ← get_env, let decls := e.filter (λ d, ¬ d.is_auto_or_internal e), -- let decls := e.filter (λ d, ¬ d.to_name.is_internal), trace decls.length, -- 72149 declarations (excluding declarations auto-generated by Lean, including declarations auto-generated by attributes) insts ← decls.mfilter (λ d, is_instance d.to_name), trace insts.length, -- 7535 instances non_insts ← decls.mfilter (λ d, bnot <$> is_instance d.to_name), trace non_insts.length, -- 64614 non-instances let defs := non_insts.filter (λ d, d.is_definition), trace defs.length, -- 12715 (non-instance) definitions let nonmeta_defs := defs.filter (λ d, d.is_trusted), trace nonmeta_defs.length, -- 9814 non-instance non-meta definitions let thms := non_insts.filter (λ d, d.is_theorem), trace thms.length, -- 50062 (non-instance) theorems let defs_incl_inst := decls.filter (λ d, d.is_definition), trace defs_incl_inst.length, -- 20196 definitions (including instances marked as definitions) skip
The numbers on the website also include the 1100+ inductive types/structures as definitions, but I'm not exactly sure what declarations are exported in the
If you compare the 50k theorems to the 10k non-instance non-meta definitions, that ratio makes more sense.
Kevin Buzzard (Mar 19 2021 at 19:18):
woo 50023 :-)
Last updated: May 14 2021 at 14:20 UTC