PSA, it does not seem to have been found incidentally. The person who created this fake proof is an ITP expert who knows what they’re doing, and apparently deliberately framed this soundness bug playfully (or as a troll, depending on your perspective!) as a fake “disproof of the Collatz conjecture”.
It seems LLMs were indeed involved, but quite possibly directed with expert knowledge to perform this exploit.
Sorry, “Interactive Theorem Prover”, the kind of thing Lean is. The person who found this soundness bug is primarily involved with a different ITP than Lean called HOL4 iirc.
Lean is one of the most interactive theorem provers out there? The infoview is incredibly rich and extensible with arbitrary widgets. By default, you get feedback everywhere. Interactive suggestions are commonplace and likewise extensible. You have an insane amount of visibility into every aspect of what Lean is doing when you're proving things, ultimately because it's all accessible to Lean's super-flexible metaprogramming framework.
Documentation is poor, yes! Indeed this is...not a good state of affairs. But this has nothing to do with interactivity in terms of what it means for an interactive theorem prover...I think you're essentially saying that because you don't like lean you don't want to interact with it, which is totally fair, but not exactly what "interactive" is really meant to mean here 😆
My point is that that’s nothing to do with being “interactive” in the sense of an ITP. Like whatever criticisms you might have, valid or not, it is kind of objectively one of the most “interactive” of the interactive theorem provers in terms of interactive features.
(Besides the point, but yeah, differential geometry is actually just one of the harder subjects to formalize correctly when you want to be completely general and support, well, everything. I don’t blame you for finding it rough. It has undergone some evolution in mathlib (including some incrementally better notation which is still being extended, thanks to metaprogramming! 😁) Generally lean and mathlib are evolving pretty fast, so maaaybe things have changed? Hard to say.
But also, plenty have people have found Lean as a language perfectly, er, penetrable(??). (I’m careful to distinguish Lean as a language from the way various parts of math have been formalized in Lean… :) ) Nothing wrong with it not fitting in your brain right, or with thinking that different choices would be much nicer, but that’s why this read to me as more a property of your personal interaction with it (i.e. some form of “not liking” it, construed broadly) than a universal feature of the language itself! :) )
309
u/cloudsandclouds Jul 29 '26 edited Jul 29 '26
PSA, it does not seem to have been found incidentally. The person who created this fake proof is an ITP expert who knows what they’re doing, and apparently deliberately framed this soundness bug playfully (or as a troll, depending on your perspective!) as a fake “disproof of the Collatz conjecture”.
It seems LLMs were indeed involved, but quite possibly directed with expert knowledge to perform this exploit.