Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Postmortem for Kernel Soundness Bug #14576

leodemoura.github.io

Post reply on HN
Print view View original

51–60 of 68 posts

Re: Postmortem for Kernel Soundness Bug #14576

#51

Post by j16sdiz »

chowells wrote: post #50
logicallee wrote: post #45

Earlier quoted context omitted.

>"what is a true statement" and "what is a derivable statement" should be the same. you mention completeness in the rest of your comment, so I'm not sure how you aren't aware of this, but the famous incompleteness theorem says that for a consistent set of axioms there will always be true statements you can't prove.[1] [1] https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...

That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent. Truth is some sort of value judgment that is outside the scope of formal…

err... There are always more ---> you can't make it "compete" by adding finite number of axioms

Re: Postmortem for Kernel Soundness Bug #14576

#52

Post by Smaug123 »

markasoftware wrote: post #39
Gehinnn wrote: post #36

Has there ever been a bug that allowed to prove a previously unproven statement, without allowing the user to prove "false" by exploiting the bug directly? If every bug-exploiting proof would make it easy to prove false, putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs.

A correctness bug in a proof checker by definition means that you can prove false.

Not necessarily. For example, perhaps my ZFC first-order-logic theorem checker implicitly accidentally contains the continuum hypothesis as an axiom. This isn't inconsistent but it is a correctness bug.

(For that matter, another correctness bug is "the checker rejects all proofs". You can't prove false if you can't prove anything.)

Re: Postmortem for Kernel Soundness Bug #14576

#53

Post by logicallee »

chowells wrote: post #50
logicallee wrote: post #45

Earlier quoted context omitted.

>"what is a true statement" and "what is a derivable statement" should be the same. you mention completeness in the rest of your comment, so I'm not sure how you aren't aware of this, but the famous incompleteness theorem says that for a consistent set of axioms there will always be true statements you can't prove.[1] [1] https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...

That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent. Truth is some sort of value judgment that is outside the scope of formal…

The second paragraph of my link talks specifically about truth:

>The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e. an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.

Re: Postmortem for Kernel Soundness Bug #14576

#54

Post by alethic »

michaelfm1211 wrote: post #18

Reminds me of this: https://mathoverflow.net/questions/513742/are-we-stuck-with-... I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system…

The utility of autoformalization is not actually in confirming the correctness of human-checked results. Mathematicians have a pretty good peer review process. I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect -- though I'm sure cases exist, it's astoundingly rare.

The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere packing results in Lean weren't because the results were in doubt -- she won a Fields Medal for it, it's an extremely examined proof -- but because formalizing those results would lead to a lot of interesting and useful mathematical objects needing to be formalized as a prerequisite, which could then be merged into Lean's Mathlib and become useful for anyone working with Lean, particularly students. Having a library of idiomatic proofs available in a formal system capable of checking your work is Really Cool! Working in a proof assistant is a great way to develop mathematical maturity, especially for people who might not have an undergraduate education available to them.

(Unfortunately in the sphere packing case, the research group working on it made the mistake of trusting one of the various "AI for Math" slop companies, who promptly rugpulled them: https://arxiv.org/html/2603.03684v3)

So the short answer is "it depends on what you want". Lean is an eminently usable system for humans and LLMs alike; Metamath is uh. Not. But yes, Metamath seems to have a more trustable kernel wrt. the independent verifiers, so if that's all you're after it would be a better pick. But... there's only so many bugs Lean's kernel can have. At some point, they'll all be found.

Re: Postmortem for Kernel Soundness Bug #14576

#55

Post by twotwotwo »

twotwotwo wrote: post #43

This thread has some context. A proof-system researcher found some proof-system bugs and presented them a funny way: https://leanprover.zulipchat.com/#narrow/channel/270676-lean... A mathematically-inclined reviewer (or an LLM) can quickly identify that it's an exploit. (Two exploits; it's crafted to hit a bug in another proof checker, too.) The post gestures at this, but a natural follow-up, beyond fixing specific b…

I think this rates as too obvious to say among anyone remotely close to this, but worth noting there is a lot of distance between an exploit and any real confusion.

Proofs aren't generally machine-read-only. An exploit of a proof system kernel doesn't necessarily look like normal proof code. Exploits can be fragile: 'safe' tweaks break them. If an exploit used maliciously is found, the person sneaking it through wouldn't exactly be thanked for it. And the window for exploits overall seems to be shrinking: Lean/nanoda are easier to secure than, say, Chrome.

If someone wanted to deliberately sow confusion (my career advice is not to do that!) they would probably have better luck with a subtly wrong formalization or an informal proof. If they have prover kernel bugs, they should report them and get free T-shirts.

Still, it's cool to see how they're hardening Lean.

Re: Postmortem for Kernel Soundness Bug #14576

#56

Post by senderista »

alethic wrote: post #54
michaelfm1211 wrote: post #18

Reminds me of this: https://mathoverflow.net/questions/513742/are-we-stuck-with-... I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system…

The utility of autoformalization is not actually in confirming the correctness of human-checked results. Mathematicians have a pretty good peer review process. I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect -- though I'm sure cases exist, it's astoundingly rare. The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere…

> I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect

https://mathoverflow.net/questions/35468/widely-accepted-mat...

Re: Postmortem for Kernel Soundness Bug #14576

#57

Post by Gehinnn »

markasoftware wrote: post #39
Gehinnn wrote: post #36

Has there ever been a bug that allowed to prove a previously unproven statement, without allowing the user to prove "false" by exploiting the bug directly? If every bug-exploiting proof would make it easy to prove false, putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs.

A correctness bug in a proof checker by definition means that you can prove false.

But how obvious would that be in the proof? Especially when you don't know if the proven statement is not true/implies false. Afaik all past problematic Lean bugs clearly implied false. But could it be that a bug is used in a way that this is absolutely not clear?

For example, the bug could allow proving a=b if the hashes of the terms equal. And the only (hypothetically) known hash collision that could be used to exploit this might not lead to an obvious contradiction.

Re: Postmortem for Kernel Soundness Bug #14576

#58

Post by markasoftware »

Gehinnn wrote: post #57
markasoftware wrote: post #39

Earlier quoted context omitted.

A correctness bug in a proof checker by definition means that you can prove false.

But how obvious would that be in the proof? Especially when you don't know if the proven statement is not true/implies false. Afaik all past problematic Lean bugs clearly implied false. But could it be that a bug is used in a way that this is absolutely not clear? For example, the bug could allow proving a=b if the hashes of the terms equal. And the only (hypothetically) known hash collision that could be used to exp…

Let a and b be as you describe (hash collision), and suppose that collisions are extremely rare. We have a theorem that a=b => a+1=b+1. But in this case, a=b according to our hash-equality, but a+1!=b+1, which contradicts the theorem we've already proved.

for real problems with my statement, see your sibling comment.

Re: Postmortem for Kernel Soundness Bug #14576

#59

Post by markasoftware »

Smaug123 wrote: post #52
markasoftware wrote: post #39

Earlier quoted context omitted.

A correctness bug in a proof checker by definition means that you can prove false.

Not necessarily. For example, perhaps my ZFC first-order-logic theorem checker implicitly accidentally contains the continuum hypothesis as an axiom. This isn't inconsistent but it is a correctness bug. (For that matter, another correctness bug is "the checker rejects all proofs". You can't prove false if you can't prove anything .)

good point, I didn't think about these cases.

Re: Postmortem for Kernel Soundness Bug #14576

#60

Post by nextaccountic »

chowells wrote: post #50
logicallee wrote: post #45

Earlier quoted context omitted.

>"what is a true statement" and "what is a derivable statement" should be the same. you mention completeness in the rest of your comment, so I'm not sure how you aren't aware of this, but the famous incompleteness theorem says that for a consistent set of axioms there will always be true statements you can't prove.[1] [1] https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...

That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent. Truth is some sort of value judgment that is outside the scope of formal…

The type theory of Lean is certainly rich enough though
Post reply on HN