Sharing so that I can keep a tab on the discussion in the comments. It seems someone has already knocked 2000-ish symbols off the original Turing machine described by Aaronson and Yedidia, and bypassing Friedman's recent work on undecidable Pi-0-1 statements (which are equivalent to consistency of certain large cardinals, so complete overkill) in the process.
Take a Turing machine with n states, two symbols, and a blank tape. What's the longest it will take to halt, if it ever does? That's the nth busy beaver number, BB(n). This sequence grows really fast and is wildly uncomputable. Now Scott Aaronson and Adam Yedidia have a paper showing that BB(7918) is unknowable within ZFC set theory!
3 comments on original post
Shtetl-Optimized » Blog Archive » The 8000th Busy Beaver number eludes ZF set theory: new paper by Adam Yedidia and me
I've supervised a lot of great student projects in my nine years at MIT, but my inner nerdy teenager has never been as personally delighted by a project as it is right now. Today, I'm proud to announce that Adam Yedidia, a PhD student at MIT (but an MEng student when he did most of this work), ...
Add a comment...