6 ms·
Can you use Lean to... prove "Lean-fast" is equivalent to Lean?
by redox99 6d ago
Can 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