5 ms·
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 happe
by pharmakom 4y ago
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.
- jwolfe 4y agoIf 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?
- fallat 4y agoThey'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.
- valenterry 4y agoThere 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.
- fallat 4y agoExactly 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.
- nimonian 4y agoIdeally, we would prove the theorem that any proof the software produces must be correct.
- bawolff 4y ago> 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.