[dodobirdlord]

> OK, the way I'd figure it out is: for such a polynomial, you definitely can't find those integers. There isn't any concrete m1...m9 satisfying the condition. The stumbling block is you can't find a proof for this fact in ZFC.

If this were formalizable it would be a proof.

I encourage you to read through the excellent piece on the busy beaver function and computability. It's not entirely related, but it's fun! And it touches on the same theme as your question here, that human intuition about mathematics is weak. The writeup describes and proves the non-computability of a particular function of positive integers with definite (but non-computable!) value.

https://www.scottaaronson.com/writings/bignumbers.html

[Dylan16807]

> If this were formalizable it would be a proof.

A proof, but not a proof that can be expressed inside ZFC.

[dodobirdlord]

Obviously, the original statement has been proved to be independent from ZFC.