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] https://mathoverflow.net/questions/353514/whats-the-smallest-lambda-calculus-term-not-known-to-have-a-normal-form