May I suggest the use of Binary Lambda Calculus [1] for writing programs and measuring their size in bits?

There are many BLC programs of only a few dozen bits, comparable in complexity to 5 state TMs that need nearly 50 bits to describe, whose halting behavior is unknown.

Beyond that, there are programs like this 215 bit one for computing Laver tables [2], whose halting behavior is related to existence of large cardinals. A counterexample to Goldbach's conjecture can be found with a 267 bit program.

[1] https://tromp.github.io/cl/Binary_lambda_calculus.html

[2] https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc

May I suggest the use of Binary Lambda Calculus [1] for writing programs and measuring their size in bits?

There are many BLC programs of only a few dozen bits, comparable in complexity to 5 state TMs that need nearly 50 bits to describe, whose halting behavior is unknown.

Beyond that, there are programs like this 215 bit one for computing Laver tables [2], whose halting behavior is related to existence of large cardinals. A counterexample to Goldbach's conjecture can be found with a 267 bit program.

I decided to pose a question on mathoverflow [3] addressing the specific form of the question.

[1] https://tromp.github.io/cl/Binary_lambda_calculus.html

[2] https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc

[3] What's the smallest $\lambda$-calculus term not known to have a normal form?

May I suggest the use of Binary Lambda Calculus [1] for writing programs and measuring their size in bits?

There are many BLC programs of only a few dozen bits, comparable in complexity to 5 state TMs that need nearly 50 bits to describe, whose halting behavior is unknown.

Beyond that, there are programs like this 215 bit one for computing Laver tables, whose halting behavior is related to existence of large cardinals. A counterexample to Goldbach's conjecture can be found with a 267 bit program.

[1] https://tromp.github.io/cl/Binary_lambda_calculus.html

[2] https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc

May I suggest the use of Binary Lambda Calculus [1] for writing programs and measuring their size in bits?

There are many BLC programs of only a few dozen bits, comparable in complexity to 5 state TMs that need nearly 50 bits to describe, whose halting behavior is unknown.

Beyond that, there are programs like this 215 bit one for computing Laver tables [2], whose halting behavior is related to existence of large cardinals. A counterexample to Goldbach's conjecture can be found with a 267 bit program.

[1] https://tromp.github.io/cl/Binary_lambda_calculus.html

[2] https://codegolf.stackexchange.com/questions/79620/laver-table-computations-and-an-algorithm-that-is-not-known-to-terminate-in-zfc