Post #4200330

2026-07-29 12:27 UTC

@0xabad1dea@infosec.exchange @0xabad1dea@infosec.exchange Concretely, "I would be happy to accept that somehow that check is incorrectly implemented, and grateful for any details on what it does wrong." ---> referred to the fact that Ramana used a version of the Nanoda kernel that predated a bug fix. But they didn't know that the bug fix had landed. But that's about the specifics of using different version of an external checker. It doesn't refer to Ramana not knowing they hadn't proved Collatz In the repository you will find an earlier version of the false proof and the meta code that produced it in a separate file. Whatever you might think, this is not a big LLM fail, quite the opposite, since finding kernel bugs is not a trivial task. The LLM probably found the bug report and fix for Nanoda (an external checker) last week, and used it to sneak in an arbitrary proof term that also exploited a different bug in the default lean kernel. People want to find these things and they are hard to find. An LLM finding it like this is a good thing. The bug has since been fixed.

Replies (1)

@escape_velocity@functional.cafe 2026-07-29 12:35

@0xabad1dea@infosec.exchange Another piece of misinformation in your post is that this "someone who was right to be very skeptical of the Collatz proof, and had the expertise to study it with a fine-toothed comb, discovered it was exploiting a bug https://..." => Kiran Gopinathan minimized the metaprogramming exploit to produce a bug report. But Ramana was the one who discovered it, and they both knew they had discovered a kernel bug. You are making highly misinformed statements that show you clearly have no idea what happened.

Open ##4200328