A walkthrough would be nice, but he's got a lot of understandable material linked on that page. For example, here's an overview of the binary lambda calculus: https://tromp.github.io/cl/Binary_lambda_calculus.html

And here's a readable and fascinating post on "the largest number that's representable in 64 bits": https://tromp.github.io/blog/2023/11/24/largest-number.

If you go through these and find some interesting things, it'd be worth posting to HN.

The first 5 values are FAR easier to determine, since there's only 1 lambda term of at most 5 bits:-)

And the next few unknown values, BBλ(37).. BBλ(39) will be easier to determine too since the search space is smaller and no so-called cryptids have been identified yet (terms whose halting behaviour is closely related to unsolved math problems).

But if the effort that is being applied to researching BB(6) and BB(7), is applied to researching BBλ(37) and beyond, then we expect to run into similar difficulties of having more and more unsolved terms which do not lead to a normal form in any reasonable number of steps and also defy known techniques for proving them to lack a normal form.

There's some hope though that we'll be able to identify BBλ(49) before identifying BB(7). And while the former is known to exceed Graham's Number, the latter is only conjectured to do so, and I made a large bet with the people conjecturing it saying it won't be proven within 10 years.