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!