Dupe of https://news.ycombinator.com/item?id=49994145

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.

[dead]

[flagged]