Busy Beaver Equivalent for the Untyped Lambda Calculus
Sequence https://oeis.org/A333479 in the On-Line Encyclopedia of Integer Sequences mostly answers your question. The question of shortest term for which lack of a normal form cannot be proven in ZFC remains open, but one candidate is the 213 bit Laver program presented in https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc