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.
> 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.
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.
Dupe of https://news.ycombinator.com/item?id=49994145
Thanks! Macroexpanded:
Navier–Stokes Lost in Translation - https://news.ycombinator.com/item?id=49994145 - Oct 2026 (226 comments)
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.
> 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.
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.
[dead]
[flagged]