Re:Lean proved this program correct; then I found a bug
by brabel on Tuesday April 14, 2026 @02:33AM
(#47762009)
When the Lean runtime has bugs, all Lean applications using the Lean runtime also have those bugs. I can’t understand people trying to make a distinction here. Is your intent to have a bug free application or to just show the Lean proof kernel is solid?? The latter is only useful to Lean developers, end users should only care about the former!
[ Parent
| on HN ]
Re:Lean proved this program correct; then I found a bug
by koito17 on Tuesday April 14, 2026 @03:28AM
(#47762410)
The intent is to have a proof of some proposition. The Lean runtime crashing doesn't stop the lean-zip developers from formally modelling zlib and proving certain correctness statements under this model. On the other hand, the Lean kernel having a bug would mean we may discover entire classes of proofs that were just wrong; if those statements were used as corollaries/lemmas/etc. for other proofs, then we'd be in a lot of trouble.
When I see a title transitioning from "Lean said this proof is okay" to "I found a bug in Lean", I'm intuitively going to think the author just found a soundness (or consistency) issue in Lean.
Re:Lean proved this program correct; then I found a bug
by ctmnt on Tuesday April 14, 2026 @06:04AM
(#47763527)
There are no Lean applications other than Lean. This is an important point most of the comments are missing. Lean is for proving math. Yes, you can use it for other things; but no, no one is.
Still good to have found, but drawing conclusions past “someone could cheat at proving the continuum hypothesis” isn’t really warranted.