Hacker News Reader

Comment by pharmakom | Hacker News Reader

We make proofs so that we can be confident something is true. But what happens when the proofs get so large that no human can practically check them? What happens when the proofs are also generated by an ANN? I wonder if this stuff around proof languages will seem totally misguided in the long run.

View on HN

Ideally, we would prove the theorem that any proof the software produces must be correct.

> But what happens when the proofs get so large that no human can practically check them

The 4 colour theorem says hello from 1976.

Ultimately though proofs are not just about being confident something is true, its usually also about why something is true.

If you're confident about your proof checker being correct, then why would you not be confident about the validity of a proof that your proof checker says is correct?

They're not even touching that but it's possible. The issue is you can still write proofs that appear correct, but really, they aren't.

Exactly this. Already we have this issue with typed languages today.

Proof languages will be welcomed but we must apply discipline as we do today with type heavy languages.

There were already cases where proofs were considered true and then later flaws where found that rendered them invalid.

I think the answer is quite simple: if something happens that contradicts the proof then a lot of resources will be used to doublecheck the proof and ensure its correctness and it will just be accepted that proofs are not always 100% valid.

Reply on news.ycombinator.com