well, 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

traes 5 hours ago | parent | next [-]

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:

It's not at all a joke ... that's a severe misunderstanding of the context.

	▲	traes 4 hours ago \| parent [-]
		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!

Fascinating, and arguably an illustration of why the bifurcation of responsibility is interesting in the first place.