# Zulip Chat Archive

## Stream: general

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

.

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