Nobody wrote 13 mil lines proofs before.

I'm pretty sure you can make Lean at least 10 times faster if you unleash the agents on it.

Somebody ported Doom to run entirely in the TypeScript TYPES (not code). It took 12 days to compile.

https://www.tomshardware.com/video-games/porting-doom-to-typ...