The overall point feels strained to me.Yes, formal mathematics has such limits. We can't expect machines to be perfect and provably perfect. But the industry isn't assuming that. Why would it? Natural intelligence is not perfect or provably perfect, either.
Rather than certainty, measurement is often enough. We can't prove a program will always halt, but we can check it halts in a specific execution.
Approximation is also often all we need. Even if we can't prove that we can train a network with more than 50% success, if we can get multiple shots at that (using different data, or initial random weights, or training techniques, or something else), then we can reduce that danger exponentially. (I don't know that we have a guarantee of succeeding there, but this would be the hope, and I am not aware of anything showing it is impossible, unlike perfect provability.)
Finally, it is possible that perfect provability does work on the problems we care about. Godel and Turing etc.'s proofs rely on finding rare situations where we can't prove things - cleverly-constructed pathological cases - but perhaps human behavior does not fall into that set. Human behavior may not be a pathological case for proofs or learnability.
7/19/2026
at
8:32:54 PM
> The overall point feels strained to me.It is. This happens to some people who discover undecidability is a thing. Then they get carried away and try to generalize to other areas. Branches of this line of thinking include the concept that intelligence must be analog with infinite precision,
(this is the same line of thinking as the argument against digital audio) or intelligence must be "quantum". (Penrose).
The formal answer to the halting problem is that deterministic systems with finite memory must repeat a previous state or halt. Undecidability requires unbounded memory. Finite memory systems may have so many states and be so complex that decidability is computationally infeasible. But that's not impossibility. I used to get this objection when I was working on proof of correctness systems. We now know that some programs are hard to decide, but many useful ones are not.
If your program is anywhere near undecidable, it's probably broken. Microsoft's position with their Static Driver Verifier was that if 45 minutes of symbolic execution hadn't found a way out, you failed driver verification. This is one of those problems, like linear programming, where part of the problem space is really hard in a computational sense, but most of it isn't.
(I sometimes wonder if Penrose was on to something with his idea that the brain uses quantum effects in microtubules.[1] Penrose is a first-rate physicist. His philosophy is not as good. It's become clear that we can do artificial intelligence with acres of transistors and gigawatts of power, but the efficiency is terrible. We need either a more efficient algorithm or better hardware elements. LLM training now is like a Newcomen steam engine, where something the size of a house had the power output of a modern motorcycle engine.)
[1] https://en.wikipedia.org/wiki/Orchestrated_objective_reducti...
by Animats