The speaker says LLM autoformalization can generate large amounts of Lean mathematics that are not always expressed with Mathlib’s desired precision and economy for canonical objects.

“The Mathlib community actually finds that this, there is a little bit of a Trojan horse, like there's kind of a downside to LLM autoformalization, and that is you just end up with this profusion of Lean mathematics that are, is not always defined with exactly, like, the precision, the economy with which you want these canonical objects in Mathlib to be expressed.”