Hacker News Reader

Comment by Gehinnn | Hacker News Reader

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.

View on HN

We want Lean4 (or any other deduction system that we use, for that matter) to be correct, i.e. "what is a true statement" and "what is a derivable statement" should be the same.

"every statement that can be derived also holds" is the difficult part to show, and something we refer to as soundness. For some fancy logics, it's not even possible to show, hence the discovered Kernel Soundness Bug in Lean!

"every statement that holds can also be derived", a notion known as completeness, is often a trivial property; in practice, we use refutation completeness instead, i.e. "every statement that doesn't hold can derive false". A bug that would allow a user to prove/derive a previously unproven statement would fall under this category of "completeness bug".

However, such completeness bugs immediately show up in testing. Generally, deduction systems have two kinds of rules: a handful of rules that are enough to establish (refutation) completeness, and then a few extra rules to optimize inference. Because so few rules are needed for completeness, lots of test cases will break if one of the rules break.

I'm not actually sure how the completeness situation looks like for proper provers like Lean. It's my graduate student's hubris to assume completeness remains easy to show for more advanced systems than the Superposition calculus ;)

>"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 systems. And looking at how bizarre Gödel statements are, it's unclear if there's any particular justification for declaring them to be true or false.

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

You can make it complete, it just won't be consistent.

In fact there is a simple way to do it -- add contradictory axioms and then you can use the principle of explosion to prove any statement as true. Is such a system inconsistent and thus useless? Yes, but it is complete.

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.

The type theory of Lean is certainly rich enough though

Don't Godel's incompleteness theorems mean that completeness is a property you don't want in a prover (as it means the prover must then be inconsistent and this unsuable) and consistency is a property of the prover you cannot prove using the prover itself?

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.

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.

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.

Reply on news.ycombinator.com