There 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."
As 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!
alt Hacker News
There 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."
As 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!