# Will a small Turing machine (< 100 states) be found with behavior that cannot be characterized by mathematical proof?

The Turing machine is an abstract model of computation used for proofs in theoretical computer science. It is very simple in its formulation - a finite set of internal states, an infinitely long tape on which characters can be written, and a finite set of transition rules dictating how a current state and current character map to: writing a new character, possibly moving the tape, and changing from one of the internal states to another. Although simple and stripped-down, the functions it can compute are equivalent to those of other models of digital computers under assumptions of unlimited time and "tape".

Theorems can be proven characterizing the behavior of very simple Turing machines - for example, a machine with only one internal state that (when it is in that state) prints a character and moves the tape ahead will never stop.

It's also known as a consequence of Godel's Incompleteness Theorem that there exist Turing machines complex enough that their behavior cannot be characterized by proof given the usual axioms of set theory (ZFC with the Axiom of Choice).

In May 2016, Adam Yedidia and Scott Aaronson published a paper demonstrating a Turing machine with 7,918 states (one tape, two possible symbols) that has behavior that is unprovable in a particular sense: the machine cannot be proven in ZFC to either run forever or not run forever, assuming that a slightly stronger formulation of set theory (Stationary Ramsey Property) is itself consistent.

In his blogpost announcing the paper, Aaronson speculated on how few states a Turing machine could have with this kind of unprovable behavior, and invited readers to improve upon this bound.

This question will resolve in the positive if, before July 1 2017, Scott Aaronson links from his blog to a paper that claims to have constructed a binary-tape-symbol Turing machine with fewer than 100 states satisfying this standard of unprovability, and Aaronson declares himself to be satisfied with the construction.

### Metaculus help: Predicting

Predictions are the heart of Metaculus. Predicting is how you contribute to the wisdom of the crowd, and how you earn points and build up your personal Metaculus track record.

The basics of predicting are very simple: move the slider to best match the likelihood of the outcome, and click predict. You can predict as often as you want, and you're encouraged to change your mind when new information becomes available.

The displayed score is split into current points and total points. Current points show how much your prediction is worth now, whereas total points show the combined worth of all of your predictions over the lifetime of the question. The scoring details are available on the FAQ.

Note: this question resolved before its original close time. All of your predictions came after the resolution, so you did not gain (or lose) any points for it.

Note: this question resolved before its original close time. You earned points up until the question resolution, but not afterwards.

This question is not yet open for predictions.

#### Thanks for predicting!

Your prediction has been recorded anonymously.

Want to track your predictions, earn points, and hone your forecasting skills? Create an account today!