3 ms·
It's not at all a joke ... that's a severe misunderstanding of the context.
by jibal 2mo ago
It's not at all a joke ... that's a severe misunderstanding of the context.
- traes 2mo agoThere 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 agoIndeed. 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.