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:
replyhttps://leanprover.zulipchat.com/#narrow/channel/270676-lean...
It's not at all a joke ... that's a severe misunderstanding of the context.
replyThere is no evidence that I can find for the claim "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."
replyAs I currently understand it, all we know is that:
- a mathematician produced a Lean-verified counterexample to the Collatz conjecture, demonstrating a bug in the kernel
- he claims that LLMs were involved somehow but pointedly refuses to specify how
- he admits that he knew about the bug before publishing the counterexample to his repository.
Perhaps not a joke (although it sure seems to me like they discovered a bug and thought falsely disproving the Collatz conjecture would be a flashy way to announce it), but at best extremely sensationalized by the above description. If you have additional context I would be happy to hear it!
Indeed. It seems to me much more likely that the AI was directed to look for bugs in Lean, found one, and then it was directed to write a proof specifically targeting the bug.
replyFascinating, and arguably an illustration of why the bifurcation of responsibility is interesting in the first place.
reply