50000 theorems in mathlib

Stream: general

[Kevin Buzzard]

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]

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 export_db.json.

If you compare the 50k theorems to the 10k non-instance non-meta definitions, that ratio makes more sense.

[Kevin Buzzard]

woo 50023 :-)