alt Hacker Newswell, a bug in the Lean kernel was discovered last week by way of an LLM tricking itself and its handler into believing it had found a non-constructive proof of the existence of a nontrivial Collatz cycle, see https://infosec.exchange/@0xabad1dea/117002106099986943 and https://lipn.info/@mevenlennonbertrand/116997917683191056
Replies
danielrmay • today at 8:36 AM
Fascinating, and arguably an illustration of why the bifurcation of responsibility is interesting in the first place.
That seems to have been more of a sensationalized joke. Even your link has a disclaimer in it now. Read this chat from the researcher who did this:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...