The human-written https://github.com/AxiomMath/PrimeGapsLib adds up to 4MB of Lean so it's that far off.

Is this human-written? Axiom Math is a company building AI theorem provers, one would think this would also be heavily AI-generated.