Comment by mrbungie
8 hours 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.
Tao 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.
For 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.
I 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).
1 reply →