> Which is sobering. It's even more sobering than that: we already know that busy beaver functions hit the bounds of decidability. From Scott Aaronson's The B

> Which is sobering. It's even more sobering than that: we already know that busy beaver functions hit the bounds of decidability. From Scott Aaronson's The Busy Beaver Frontier (https://www.scottaaronson.com/papers/bb.pdf https://www.scottaaronson.com/papers/bb.pdf), BB(748) is already undecidable under ZF set theory if the latter is consistent. Aaronson even conjectures that BB(20) is undecidable under ZF theory and that BB(10) is undecidable under Peano arithmetic -- he's thinks the existing proofs still have lots of room for improvement. If BB(10) is undecidable under Peano arithmetic, then all we're left with for BB analysis is the space of very small Turing machines.