6 ms·
It'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
by stabbles 6d ago
It'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?
- redox99 6d agoCan you use Lean to... prove "Lean-fast" is equivalent to Lean?
- gcgbarbosa 6d agoMaybe, but how many centuries would it take to prove it?
- calebkaiser 6d agoYeah, in essence. This is actually a pretty cool part of working in Lean. It's a somewhat normal convention to write something in a human readable way and then write a second optimized implementation with some kindness of correctness theorem connecting them. There was a whole open "competition" for writing a faster Lean kernel/proof checker that didn't sacrifice on soundness called Lean Kernel Arena. Fun reference point: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-than-rust/ https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...
- stabbles 6d agoGreat read, thanks for sharing
- mattr03 6d agoThere's a project called lean4lean that implements lean in lean. I guess ideally, if you had a kernel optimisation idea you could do a copy of the Lean model lean4lean has created, add the optimisation, then prove your new lean is equivalent in terms of what it can prove to the old lean
- andrewchambers 6d agoIf they aren't already, or if its possible, prove that an optimized version matches the simple version...
- QwenGlazer9000 6d agoIt'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.
- andrewchambers 6d agoThey could probably vibe-optimize it if they cared. What would happen if they give an equivalent agent swarm the proof and a target to reduce runtime .
- maths_math 6d agoWhat would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...
- jchanimal 6d agoThen run the annealer and learn from the result.
- andrewchambers 6d agoI was replying to the comment about it being slow to run. I wasn't commenting on understanding it.
- devin 6d agoLet’s start with “what would happen” and run the experiment instead of starting with “they could probably”.
- mkl 6d agoKevin Buzzard. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h..., discussed recently here: https://news.ycombinator.com/item?id=49568667 https://news.ycombinator.com/item?id=49568667
- dist-epoch 6d agoNobody 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-typescript-types-took-3-5-trillion-lines-90gb-of-ram-and-a-full-year-of-work https://www.tomshardware.com/video-games/porting-doom-to-typ...
- advisedwang 6d agoBut 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.
- dooglius 6d agoWeren'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.
- kingstnap 6d agoPerformance problems in theorem provers is an old topic. I remember watching this and it was fun. https://youtu.be/m-iGCCuHBvY https://youtu.be/m-iGCCuHBvY [Talk] 10 years of superlinear slowness in Coq (2022)
- jcalx 6d ago> 230 GB of RAM "I have discovered a truly marvelous proof of this, which my memory is too small to contain..."
- throwup238 6d ago“Big data”!
- symfoniq 6d agoThey’re using Electron to write proofs now?
- bawolff 6d agoDoes it really matter? You really only need to run it once.
- skew-aberration 6d agoSure, but to clarify the article is describing formalization (writing a correct program), not verification (compiling said program). The author is not making the same comparison. Verification is also open ended (not sure about lean specifically) - you could in theory give just the Navier-Stokes problem definition to an ATP and let it run.
- aaron695 6d ago[dead]