P≠NP deserves a little more credit than you give it. To interpret the claim correctly, we need to notice P and NP are classes of decision problems, not classes of proof systems for decision problems. You demonstrate that for a fixed proof system it is possible that generating proofs is easier than verifying proofs. However, if we fix a decision problem and allow any valid (i.e. sound and complete) proof system, then verifying cannot be harder than generating. Indeed, let S1 be some proof system and A an algorithm for generating proofs (i.e. an algorithm that finds a proof if a proof exists and outputs “nope” otherwise). Then, we can construct another proof system S2, in which a “proof” is just the empty string and “verifying” a proof for problem instance x consists of running A(x) and outputting “yes” if it found an S1-proof and “no” otherwise. Hence, verification in S2 is no harder than generation in S1. Now, so far it’s just P⊆NP, which is trivial. The non-trivial part is: there exist problems for which verification is tractable (in some proof system) while generation is intractable (in any proof system). Arguably there are even many such problems (an informal claim).
P≠NP deserves a little more credit than you give it. To interpret the claim correctly, we need to notice P and NP are classes of decision problems, not classes of proof systems for decision problems. You demonstrate that for a fixed proof system it is possible that generating proofs is easier than verifying proofs. However, if we fix a decision problem and allow any valid (i.e. sound and complete) proof system, then verifying cannot be harder than generating. Indeed, let S1 be some proof system and A an algorithm for generating proofs (i.e. an algorithm that finds a proof if a proof exists and outputs “nope” otherwise). Then, we can construct another proof system S2, in which a “proof” is just the empty string and “verifying” a proof for problem instance x consists of running A(x) and outputting “yes” if it found an S1-proof and “no” otherwise. Hence, verification in S2 is no harder than generation in S1. Now, so far it’s just P⊆NP, which is trivial. The non-trivial part is: there exist problems for which verification is tractable (in some proof system) while generation is intractable (in any proof system). Arguably there are even many such problems (an informal claim).