You have to first understand what is the problem here. A problem is usually a relation between inputs and outputs. The complexity is a measure of difficultly for algorithms to obtain input from the output. A single instance of a problem like the one you have are trivial, since there exists an algorithm that would output the answer (whether it is provable, refutable, or neither). However from the practical point of view this is not of much use.
Asking for $\mathsf{NP}$-hardness of an instances is a confusion that is not uncommon among non-experts in theoretical computer science. The reason for this confusion is that in algorithms/complexity courses, many students mistakenly view $\mathsf{NP}$-hardness as "not solvable in practice" or "no algorithm". $\mathsf{NP}$-hardness does NOT mean that the instances of the problem cannot be solved in practice (take for example SAT), it neither means that there are no algorithms, and it doesn't even mean that there is no efficient/polynomial time algorithm for the problem ($\mathsf{P}$ vs. $\mathsf{NP}$ is still an open problem in theoretical computer science and it doesn't seem that we are close to answer it).
I am guessing that what you really want to ask is if it is possible to use computer to find the answer to $\mathsf{P}$ vs. $\mathsf{NP}$. 915
But this is not a very precise question: what do we mean by using computers to solve an instance of a problem?
Let me try to clarify this: assume that I know the answer to the question, and I write a one line program that always outputs the same correct answer (e.g. the answer to the question is YES and my program is cout<<"YES";). Do we consider this as using computers to find the answer to the question? I would assume no.
Another situation to understand the issues: assume that I have a brute-force algorithm and it finds the answer after say 1 billion years. It is an answer after a finite time, so it is a constant time algorithm However it is not really useful for us, since presumably we want to know the answer in a reasonable amount of time (say before we die). What is a reasonable amount of time? It is not a precise concept.
In summery,
* a problem instance cannot be $\mathsf{NP}$-hard, an problem instance is trivial from complexity perspective (there exists an algorithm that outputs the correct answer in constant time, we know it is one of the 3 programs (always output "YES", always output "NO", always output "UNDECIDABLE") but we don't know which of these 3 programs correctly solves the problem.
* $\mathsf{NP}$-hardness is a theoretical concept for a general instance of problems, it doesn't imply that we cannot solved a problem on instances we care about in practice (SAT is $\mathsf{NP}$-hard but in practice SAT-solvers work amazingly well on instances that some industries case about and understanding why this is the case is an on-going research topic).
* in practice often we don't care about general inputs, we care about a specific subclass of inputs, and on those inputs we might be able to solve the problem. However we should understand that our algorithm will not work on general examples. Any algorithm that works well on some subsets of inputs needs to exploit some properties of those inputs. If we don't have any idea about the particular properties of our instance then we are in a situation similar to the general case inputs.
* when we don't know any particular property of an instance of a problem we think of it at that time as being hard as general case.
One final point: even if $\mathsf{P}=\mathsf{NP}$ and we can solve SAT and proof search for proofs of a given length efficiently (given $\varphi$ and $n$, is there a proof of length $n$ for $\varphi$ in theory $T$, think of $T$ as ZFC for simplicity), it is possible that it won't help much with finding a proof of that fact for various reasons, e.g.:
* although the statement is true, there is no proof of it, so current axioms of mathematics are incapable of settling the question positively or negatively,
* we have an efficient algorithm for searching for proofs of given length, however the constants in the running time of the algorithm are huge, so even though the algorithm is polynomial time, it is not a practical algorithm (e.g. running time is $10^{1000}n^{500}$).
And similarly if $\mathsf{P}\neq\mathsf{NP}$, it doesn't mean that there isn't a short proof of this particular statement in $T$. 603