Yes! I think that working with Mathlib is the best long term solution, because it's how people already collaborate on building out the formal "universe of mathe

Yes! I think that working with Mathlib is the best long term solution, because it's how people already collaborate on building out the formal "universe of mathematics." We want to speed that up, and hopefully we'll cover all of the common topics very soon!