I take a very dim view of slopping out 500kloc and then giving it to unpaid experts to perform the actual work of checking it (confirmed at https://leanprover.zulipchat.com/#narrow/channel/583336-Auto... that this is what they did), especially given the reported incorrectness of the code (https://leanprover.zulipchat.com/#narrow/channel/583336-Auto... or https://leanprover.zulipchat.com/#narrow/channel/583336-Auto... for example).

They say in the Lean Zulip thread that this is actually intentionally a "low quality" release (https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...); the paper notes that the quality is "inferior to that of expert-written Lean code". Then again, "Our results suggest that formalizing the core textbook infrastructure of modern mathematics is within reach".