I'm enjoying learning about these hard problems, but this line about credit made me chuckle:

> We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness

Offering to take responsibility for the correctness of a proof written in Lean feels like volunteering to be the fall guy in case someone finds a flaw in basic arithmetic, no?

▲

DroneBetter 5 hours ago | parent | next [-]

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:

https://leanprover.zulipchat.com/#narrow/channel/270676-lean...

▲

jibal 4 hours ago | parent [-]

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!

▲

danielrmay 5 hours ago | parent | prev [-]

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

▲

traes 5 hours ago | parent | prev | next [-]

I'm not an expert at it myself, but my understanding is there are numerous ways to "cheat" in a Lean proof (via `sorry` and similar). They're taking responsibility for fully verifying that none of these cheats were used (and that the theorem statements themselves were all correctly formalized.)

▲

emil-lp 5 hours ago | parent | prev [-]

No, the correctness isn't for the "inside the Lean proofs", but for the translation of "human language math" and its formal Lean variant.

▲

danielrmay 5 hours ago | parent [-]

I see. It still feels like a bit of an oddly solemn way of saying "this is the part we admit responsibility for"

	▲	baq 5 hours ago \| parent \| next [-]
		It’s more than you get from free software - you get no proofs, no warranties and any responsibility of its authors are their pure good will. Reminder lean proofs are software!
	▲	emil-lp 5 hours ago \| parent \| prev [-]
		Well, to be fair, with Lean proofs, that's the only thing there is (unless I'm missing something).