Not qualified to answer, but my thought is that if you have a statement that is true that cannot be proven, you could write a program whose correctness implies the statement, then proving the program correct amounts to proving something that can not be proven.