Comment by zodiac

Tokens are not the bottleneck for filling in these gaps in mathlib. Human review and growing the specialized expertise needed for human review are. https://leanprover-community.github.io/contribute/index.html...