While Goodstein sequences do get really long quite fast, they're not that easy to code. This binary lambda calculus program [1] may be the shortest possible, bu

While Goodstein sequences do get really long quite fast, they're not that easy to code. This binary lambda calculus program [1] may be the shortest possible, but still takes 351 bits. Meanwhile, in a mere 215 bits, we can encode a Laver table program [2] that potentially grows so much faster than Goodstein, that it's not even provable in ZFC [3]. [1] https://github.com/tromp/AIT/blob/master/goodstein.lam https://github.com/tromp/AIT/blob/master/goodstein.lam [2] https://github.com/tromp/AIT/blob/master/laver.lam https://github.com/tromp/AIT/blob/master/laver.lam [3] https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc https://codegolf.stackexchange.com/questions/79620/laver-tab...