4 ms·
Probably an AI-written Lean proof is very different to how a human would write it, and some may say it's more like mathy neuralese. For sure it works but it is
by mrbungie 24d ago
Probably an AI-written Lean proof is very different to how a human would write it, and some may say it's more like mathy neuralese. For sure it works but it is not human-friendly and needs to be transformed into something more readable and digestible to be able to extract insights from it.
Not that different from when trying to read an out-of-control vibe coded codebases, or an sloppy AI long email that someone may send you at 9 AM.
- meken 24d agoTao has a spiel in his recent interview with Dwarkesh where he says that AIs are very good at explaining things - so just have the AI explain the proof in a human-friendly way.
- mrbungie 24d agoFor sure, but this was supposedly ~18 million dollars of compute, afaik 100 pages paper / lean proof and only god knows how many bytes of chat interactions + thought traces. Scale matters.
- meken 24d agoI bet it can be decomposed quite nicely though. At the top level, there are probably only like five steps. Dig as deep as you want into any of those steps (i.e. engineering).
- mrbungie 24d agoHopefully. We'll need to wait until mathematicians confirm how easy it is to digest whatever GPT did.