Comment by le-mark

> the mathlib has many gaps and lacks many basic theories.

Filling these gaps would be a great use of llm tokens!