[svat]

I'm sure you know this, but even very simple/short programs can have complex behaviours that put them out of reach of computer scientists with present-day knowledge. For example, short programs can encode things like the Goldbach conjecture, the Collatz conjecture, or the Riemann Hypothesis. For example, does this program (written in Python, but translate to your computational system) halt?

    def isprime(n): return n > 1 and all(n % d for d in range(2, n))
    def goldbach(n): return any(isprime(p) and isprime(n - p) for p in range(2, n))
    n = 4
    while goldbach(n): n += 2

(See also the recent https://www.quantamagazine.org/amateur-mathematicians-find-f... which describes how hard it was to prove things even about puny 5-state Turing machines, and that already with just 6 states there is one "antihydra" that encodes Collatz-like behaviour and will probably be hard to prove anything about.)

[User23]

Absolutely. And frankly I think that’s very exciting. If I had to lay a wager I reckon if those problems will be solved by a human intelligence, the most likely method will be through taking advantage of that correspondence and proving some tractable representation of the appropriate program halts.

Like many people I had a casual go at it for Collatz. It was a humbling experience of course, but it did nothing to convince me some more capable person can’t eventually manage it.