Comment by throw567643u8

4 hours ago

13 million lines of code, a lot of which is new to Mathlib. So it hasn't built on what is already there but synthesised a bunch of new stuff.

LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.