If AI is water, Lean is the pipe and collatz is a clog on one end, then surely we'll find the cracks.
(In practice, there’s also the possible error that the proved formal statement means something different than what you intended it to mean.)
Things like this aren't too surprising, given that even much simpler type checkers like Rust's have soundness issues occasionally. I think it's very important to view verified results not as an absolute and unbreakable guarantee, just an extraordinarily strong one where (1) the surface area for soundness issues has been painstakingly minimized and (2) any realized soundness issues are taken very seriously and fixed in short order.
Use Coq or Isabelle or any other decent theorem prover. Lean is just hyped.
- Probably too close to corporations.
- Does not care about slop.
We have seen many projects that adopted AI under corporate pressure circle the drain. Often the corporations themselves backpedaled after some months.
Beyond that it looks like a pretty simple oversight. Coq and Isabelle have also had 'prove False' bugs, it isn't the end of the world. Stuff like this happens.
I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system like Metamath?
juhopitk•1h ago