alt Hacker NewsIt's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it).
To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?
Replies
Can you use Lean to... prove "Lean-fast" is equivalent to Lean?
But what hardware was the verification vs agents on? Because you are likely comparing verification on a single beefy machine (say XX TFLOPS total) to agents running on a substantial inference cluster (say XXXX TFLOPS). So you're 1 order of magnitude might actually be 2-4 orders of magnitude.
Weren't the agents massively parallel, whereas the lean verifier presumably is not? Also, I presume said agents were themselves running the verifier on their own parts many times.
If they aren't already, or if its possible, prove that an optimized version matches the simple version...
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...
It's because anthropic vibemathed it. I forgot the name but some other guy is working on a handwritten version of it and I bet it'll be more than just 1 magnitude faster.