8 ms·

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 Le

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?

emil-lp 2mo ago
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 2mo ago
  I see. It still feels like a bit of an oddly solemn way of saying "this is the part we admit responsibility for"
  - emil-lp 2mo ago
    Well, to be fair, with Lean proofs, that's the only thing there is (unless I'm missing something).
  - baq 2mo ago
    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!
  - jhanschoo 2mo ago
    Traditionally, a mathematician would be implicitly responsible for all that (if they were to publish Lean code) and also the intellectual work that led to the artifact of the mathematical paper (and code, if part of the contribution). This statement should rather be read as an acknowledgement of limitation of authorship from the implicit, traditional understanding.
traes 2mo ago
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.)
- rencrisa 2mo ago
  Even beyond cheating with sorries or kernel bugs, the lean encoded theorems (or specifications) must be checked by humans to see if they truly mirror the real theorem authentically.
DroneBetter 2mo ago
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!
      - 2mo ago
rencrisa 2mo ago
It seems that a lot of folks misunderstand the guarantees that lean provides. I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications), that the lean proofs are checked against, indeed correctly encode the real theorems. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.

emil-lp 2mo ago

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 2mo ago
I see. It still feels like a bit of an oddly solemn way of saying "this is the part we admit responsibility for"
- emil-lp 2mo ago
  Well, to be fair, with Lean proofs, that's the only thing there is (unless I'm missing something).
- baq 2mo ago
  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!
- jhanschoo 2mo ago
  Traditionally, a mathematician would be implicitly responsible for all that (if they were to publish Lean code) and also the intellectual work that led to the artifact of the mathematical paper (and code, if part of the contribution). This statement should rather be read as an acknowledgement of limitation of authorship from the implicit, traditional understanding.

traes 2mo ago

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.)

rencrisa 2mo ago
Even beyond cheating with sorries or kernel bugs, the lean encoded theorems (or specifications) must be checked by humans to see if they truly mirror the real theorem authentically.

DroneBetter 2mo ago

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!
    - 2mo ago

rencrisa 2mo ago

It seems that a lot of folks misunderstand the guarantees that lean provides. I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications), that the lean proofs are checked against, indeed correctly encode the real theorems. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.