If Lambda Calculus and AIT team up, then this happens: https://tromp.github.io/cl/Binary_lambda_calculus.html https://tromp.github.io/cl/Binary_lambda_calculus

If Lambda Calculus and AIT team up, then this happens: https://tromp.github.io/cl/Binary_lambda_calculus.html https://tromp.github.io/cl/Binary_lambda_calculus.html This has recently led to a functional Busy Beaver at https://mathoverflow.net/questions/353514/whats-the-smallest-lambda-calculus-term-not-known-to-have-a-normal-form https://mathoverflow.net/questions/353514/whats-the-smallest... https://oeis.org/A333479 https://oeis.org/A333479