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?
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
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...
loading story #49132754
Fascinating, and arguably an illustration of why the bifurcation of responsibility is interesting in the first place.
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.)
No, the correctness isn't for the "inside the Lean proofs", but for the translation of "human language math" and its formal Lean variant.
I see. It still feels like a bit of an oddly solemn way of saying "this is the part we admit responsibility for"
loading story #49139720
loading story #49132287
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!