As the article mentions, the generalized continuum hypothesis has been proven to be undecidable in ZFC, and I believe specific Diophantine equations have been p

As the article mentions, the generalized continuum hypothesis has been proven to be undecidable in ZFC, and I believe specific Diophantine equations have been proven to be undecidable. Axiom of Choice of course is undecidable from the other ZF axioms/axiom schemas. Answering questions about a presentation of a group is provably undecidable in general but since it is a kind of halting problem that makes sense.