The Collatz conjecture is "obviously" (i.e. probabalistically) true, so it's frustrating to not be able to turn that into a proof. PA doesn't matter, there's n

The Collatz conjecture is "obviously" (i.e. probabalistically) true, so it's frustrating to not be able to turn that into a proof. PA doesn't matter, there's no known approach to proving it with stronger theories either. Of course many other propositions like the twin prime conjecture are in the same situation. Goodstein's theorem by contrast is obviously provable in slightly stronger theories than PA, and it involves a fast-growing sequence which suggests it's out of weaker theories' reach. In fact it encodes ordinals up to eps_0 in a natural way, so its equivalence to CON(PA) is unsurprising. The Collatz conjecture is nothing like that. It's beguilingly simple by comparison.