Comment by dddbbb

The author of the Metamath Zero paper is actually one of the most active contributors to the project described in the article[0].

[0]: https://leanprover-community.github.io/mathlib_stats.html