from Scott Aaronson's blog: The 8000th Busy Beaver number eludes ZF set theory: new paper by Adam Yedidia and Scott A. http://www.scottaaronson.com/blog/?p=2725
Today, Im proud to announce that Adam Yedidia, a PhD student at MIT (but an MEng student when he did most of this work), has explicitly constructed a one-tape, two-symbol Turing machine with 7,918 states, whose behavior (when run on a blank tape) can never be proven from the usual axioms of set theory, under reasonable consistency hypotheses. Adam has also constructed a 4,888-state Turing machine that halts iff theres a counterexample to Goldbachs Conjecture, and a 5,372-state machine that halts iff theres a counterexample to the Riemann hypothesis. In all three cases, this is the first time weve had an explicit upper bound on how many states you need in a Turing machine before you can see the behavior in question.
Includes a very short summary of work on BB(5) & BB(6), with a pointer to Marxen's page. Uses Lagarias's equivalence for Riemann. Rich