3 ms·

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

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 https://infosec.exchange/@0xabad1dea/117002106099986943 and https://lipn.info/@mevenlennonbertrand/116997917683191056 https://lipn.info/@mevenlennonbertrand/116997917683191056

traes 2mo ago
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-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/near/613480044 https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
- jibal 2mo ago
  It's not at all a joke ... that's a severe misunderstanding of the context.
  - traes 2mo ago
    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!
    - zahlman 2mo ago
      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.
danielrmay 2mo ago
Fascinating, and arguably an illustration of why the bifurcation of responsibility is interesting in the first place.

traes 2mo ago

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-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/near/613480044 https://leanprover.zulipchat.com/#narrow/channel/270676-lean...

jibal 2mo ago
It's not at all a joke ... that's a severe misunderstanding of the context.
- traes 2mo ago
  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!
  - zahlman 2mo ago
    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.

danielrmay 2mo ago

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