This headline is completely wrong. The proper coding analogy is more like, the natural-language paper was the "design document" before coding it up, then when coding it up as Lean4 proofs, specific details were realized to be slightly off[1] and corrected while writing the implementation in code as machine-checkable proofs. Which I'm sure is an extremely relatable situation for most of us here. But the paper or "design document" wasn't corrected afterwards.
I also think this "paper then code" approach is now obsolete. The modern way, in AI-assisted workflows, is to first iterate on "derivation sketch <-> machine-checkable proof" incrementally building out your result. You can of course leave `sorry` placeholders along the way and fill them in, so it's not like you're restricted to going entirely bottom-up. Then, once you have a `sorry`-free proof of your top-level statements (theorems) of interest, then you work on writing up the exposition in LaTeX based on the lean code.
1. See https://arxiv.org/abs/2610.08144 for details, but an example they point out is that a key bound required 5 additional orders of derivatives (and stated in Lean that way), but the paper claimed that the bound held with only four more derivatives.
> I also think this "paper then code" approach is now obsolete. The modern way, in AI-assisted workflows
To call the approach obsolete and refer to a "modern way" to use an LLM seems like a stretch when critiquing the approach used by a frontier lab a month ago.
This headline is completely wrong. The proper coding analogy is more like, the natural-language paper was the "design document" before coding it up, then when coding it up as Lean4 proofs, specific details were realized to be slightly off[1] and corrected while writing the implementation in code as machine-checkable proofs. Which I'm sure is an extremely relatable situation for most of us here. But the paper or "design document" wasn't corrected afterwards.
I also think this "paper then code" approach is now obsolete. The modern way, in AI-assisted workflows, is to first iterate on "derivation sketch <-> machine-checkable proof" incrementally building out your result. You can of course leave `sorry` placeholders along the way and fill them in, so it's not like you're restricted to going entirely bottom-up. Then, once you have a `sorry`-free proof of your top-level statements (theorems) of interest, then you work on writing up the exposition in LaTeX based on the lean code.
1. See https://arxiv.org/abs/2610.08144 for details, but an example they point out is that a key bound required 5 additional orders of derivatives (and stated in Lean that way), but the paper claimed that the bound held with only four more derivatives.
> I also think this "paper then code" approach is now obsolete. The modern way, in AI-assisted workflows
To call the approach obsolete and refer to a "modern way" to use an LLM seems like a stretch when critiquing the approach used by a frontier lab a month ago.
Dupe of https://news.ycombinator.com/item?id=49994145
Aka, no one at OPENAI is doing much to seriously vet their claims.
No wonder trumps moving to AI.