Is there an open mathematical conjecture which has been shown not to be provable in Peano Arithmetic before (possibly) being proved true?

87 Views Asked by At

There are several mathematical statements $\varphi$ about the natural numbers which are known to be true and known not to be provable in Peano Arithmetic (c.f. Gödel's incompleteness theorem, Paris-Harrington theorem, Kirby-Paris theorem...). In all such instances I know of, $\varphi$ was first shown to be true in "standard mathematical practice" and only later logicians showed that $\varphi$ is not provable in PA.

Is there any example of statement $\varphi$ about the natural numbers which is not known to be true but already known not to be provable in PA? Or, at least, is there any such example which had such a status in the past (i.e., until actually being proven true)?