It is unprovable (and undecidable!), but that does not make it “true” any more than it makes it false. Indeed, there have been compelling arguments why it should be false as well as compelling arguments why it should be true. It can depend on what other axioms you might want or need to take as true, e.g. Martin’s maximum.
Which “it” are you refering to?
Sorry for replying to a question for @DPRK but “it” could be any proposition that is “true” but provably undecidable in some system. We could always create a new system by including its negation as an axiom. The resulting system would be as consistent as the original and the proposition would be false by definition.
The Continuum Hypothesis
That is true. In set theory the truth of the continuum hypothesis may be determined by other axioms. For example (unless I confused something) you cannot have both the “proper forcing axiom” and the continuum hypothesis. On the other hand, “every set is constructible” implies the continuum hypothesis.
Right; thanks.
I certainly agree: for doing long symbol manipulation tasks, computers are almost certainly less likely to make a mistake than a human. But again, as you say, that’s probably not the interesting part. The creative step is framing the problem in a way that it can be ‘crunched’ by brute force exhaustion.
GPT is well known for generating complete bullshit.
Have you looked into independent verification of any of these?
According to Wikipedia they are all examples of true but unprovable theorems.