Simple example of halting-unprovable Turing machine

Is there a simple example of a Turing machine $M$, such that whether $M$ halts or not on the empty input cannot be proved within the current mathematical system?

Specifically, I'm curious whether there exists an example simple enough that the state transition of the Turing machine can be drawn as a reasonably-sized diagram.

• look at the answers of this thread: cstheory.stackexchange.com/questions/20978/… Jan 23, 2015 at 0:53
• one can take any halting problem with arbitrary input and encode that into the start/ initialization states of the TM to write the input to the tape. so Turings classic problem applies here with simple adjustment. it is known from some research on "small TMs" the halting problem is encodable in some fairly small TMs.
– vzn
Jan 23, 2015 at 18:34

Take the "current mathematical system" $S$ and an undecidable sentence $P$ for $S$. Consider the Turing machine $T$ which enumerates all theorems of $S$ and halts if it ever enumerates either $P$ or $\lnot P$. System $S$ cannot decide whether $T$ halts.
Note that such a $T$ does not halt.
• See here, here and here for discussion of some specific $2$-symbol Turing machines with ZFC-independent halting problem, recently created in essentially the manner you describe. It appears that the number of states required for such a machine is now at $1919$, and quite sure to decrease further. Jun 29, 2016 at 22:28