When I mentioned writing a symphony I was essentially referring to your quote from Scott Aaronson and I am also aware that some known proofing methods have been

When I mentioned writing a symphony I was essentially referring to your quote from Scott Aaronson and I am also aware that some known proofing methods have been shown not to be strong enough to settle the question. I don't really buy into most of the examples of the quote. For example it is already a complex problem to quantify what makes a symphony a great symphony, once you solved this it of course becomes easy to recognize great symphonies. To write a great symphony you could then just exhaustively search the space of symphonies and rate them until you find a great one. But does it really sound highly implausible to you that once you figured out what makes a symphony a great symphony you could use that knowledge to prune the search space and discover great symphonies much faster that using exhaustive search? And the fact that known techniques are not good enough to settle the question doesn't sound like a surprise to me either. The very fact that the problem is not yet settled means that the usual approaches don't work and we have to use known things in an innovative way or come up with something entirely new. So that some things don't work hardly comes as a surprise but not even this implies that P == NP is more likely right or more likely wrong, it just says that figuring it out is hard. You could maybe argue that it is evidence for the problem being independent from ZFC or whatnot if we and our tools constantly fail to settle the problem one way or the other.