You've described a very short algorithm for finding a very long proof. But what the algorithm finds is indeed a very long proof, not a short one, and the reason

You've described a very short algorithm for finding a very long proof. But what the algorithm finds is indeed a very long proof, not a short one, and the reason I say that is because the short algorithm description you gave doesn't convince me of the truth of the statement "Every coloring of positive integers up through 7825 contains a monochrome Pythagorean triple"; you could give similarly short descriptions of algorithms searching for hypothetical proofs of any number of false claims. It's only the long-ass step-by-step completed execution of that algorithm which does the convincing.