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. Finally, once you have a `sorry`-free proof of your top-level statements (theorems) of interest, you can then 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.
nsagent [3 hidden]5 mins ago
> 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.
jey [3 hidden]5 mins ago
Shrug. It's how I do my research now. There were too many mathematical errors when I had agents writing LaTeX directly, even with adversarial reviews, so now I only read stuff that's been formalized, with whatever kinks worked out along the way.
HN.zip
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. Finally, once you have a `sorry`-free proof of your top-level statements (theorems) of interest, you can then 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.
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.
No wonder trumps moving to AI.