Adam Yedidia, a PhD student at MIT, has constructed a one-tape, two-symbol Turing machine with 7,918 states whose behavior cannot be proven from the axioms of set theory. Yedidia has also constructed Turing machines that halt if there is a counterexample to Goldbach’s Conjecture or the Riemann Hypothesis. This is the first time an explicit upper bound on the number of states needed for these behaviors has been determined. Yedidia’s work was made possible by the creation of a new programming language called Laconic. The research paper and code can be found online.
https://scottaaronson.blog/?p=2725