> The busy beaver game is all about the behavior of Turing machines A busy beaver for lambda calculus is even easier to define: the maximum normal form size o

> The busy beaver game is all about the behavior of Turing machines A busy beaver for lambda calculus is even easier to define: the maximum normal form size of any closed lambda term of size n (or 0 if none exists). The series [1] starts as 0, 0, 0, 4, 0, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 22, 24, 26, 30, 42, 52, 44, 58, 223, 160, 267, 298, 1812, 327686, 38127987424941, 578960446186580977117854925043439539266349923328202820197287920039565648199686 Results are more fine grained than for TMs because these sizes are in units of bits (lambda and application measuring as 2 bits, and a variable bound by n'th enclosing lambda as n+1 bits). Graham's number is surpassed within 114 bits, while the smallest known TM for surpassing it takes 225 bits to describe. [1] https://oeis.org/A333479 https://oeis.org/A333479