> If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway.
We cannot, as a human might be able to intuitively devise proof that might be quite large in the target language but easily constructible in a separate one.
We cannot, as a human might be able to intuitively devise proof that might be quite large in the target language but easily constructible in a separate one.