Not all true theorems have a proof? (what does that even mean)
Picture an enormous polynomial f(x, y, …) with integer coefficients: something like 3x^2 − 6y + 5 but bigger. Now, if the Diophantine equation f(x, y, …) = 0 has a solution then this can easily be proved—you just have to plug in the numbers and calculate the result. (Even if you’re not told the numbers in advance, you can iterate over all possible arguments and still prove the result in a finite time.)
But now suppose that this particular f doesn’t have any solutions. (Think about whether you want to deny that the previous sentence is meaningful—personally I think it is).
Can we necessarily prove it doesn’t have any solutions? Well, there’s no algorithm that can correctly decide whether f has a solution for all Diophantine equations f. (See “Hilbert’s Tenth Problem”.) So certainly there exists an f, without any solutions, such that “f has no solutions” is not a theorem of (say) ZFC set theory. (Because for any formal axiomatic system, one can write down an algorithm that will enumerate all of its theorems.)
Perhaps, like Roger Penrose, you think that human mathematicians have some magical non-algorithmic ‘truth-seeing’ capability. Unfortunately, human thought being non-algorithmic would require that physics itself be uncomputable i.e. an accurate computer simulation of a brain solving a mathematical problem would be impossible even in principle. Otherwise, you must conclude that some theorems of the form “this Diophantine equation has no solutions” are not humanly provable.
Picture an enormous polynomial f(x, y, …) with integer coefficients: something like 3x^2 − 6y + 5 but bigger. Now, if the Diophantine equation f(x, y, …) = 0 has a solution then this can easily be proved—you just have to plug in the numbers and calculate the result. (Even if you’re not told the numbers in advance, you can iterate over all possible arguments and still prove the result in a finite time.)
But now suppose that this particular f doesn’t have any solutions. (Think about whether you want to deny that the previous sentence is meaningful—personally I think it is).
Can we necessarily prove it doesn’t have any solutions? Well, there’s no algorithm that can correctly decide whether f has a solution for all Diophantine equations f. (See “Hilbert’s Tenth Problem”.) So certainly there exists an f, without any solutions, such that “f has no solutions” is not a theorem of (say) ZFC set theory. (Because for any formal axiomatic system, one can write down an algorithm that will enumerate all of its theorems.)
Perhaps, like Roger Penrose, you think that human mathematicians have some magical non-algorithmic ‘truth-seeing’ capability. Unfortunately, human thought being non-algorithmic would require that physics itself be uncomputable i.e. an accurate computer simulation of a brain solving a mathematical problem would be impossible even in principle. Otherwise, you must conclude that some theorems of the form “this Diophantine equation has no solutions” are not humanly provable.