Has anyone here actually looked at the Shai Ben David (SBD) result? I did a final grad project on it recently for a class on incompleteness. In my view it's not really that interesting. For learnability to be undecidable, the cardinality of the continuum (size of the reals) must exceed \aleph_k for all finite k. ZFC does not bear upon this (CH is independent of ZFC), so this is a possible setting of the world, and therefore learnability can be undecidable.

But say the size of the continuum is, e.g., \aleph_3, (in this case CH is false, but it's not "horribly false"), then SBD shows how to build a compression scheme, and thus their EMX -- estimating the maximum problem -- is "learnable". But the compression scheme whose existence they show (it's just a function whose existence they prove) can't actually be encoded, since it requires identifying a maximal element by invoking the well-ordering theorem. So there's no algorithm that enables solving the problem (though a function solving the problem exists).

This result, without further work, does not immediately say anything about the sorts of problems for which abstractions can be learned. And abstraction is at the heart of understanding and problem solving.

See e.g., https://arxiv.org/pdf/1909.08410 (§5)

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.

Yes, but does a computer system or tool or AI need to be provably correct or 100% guaranteed not to cause harm to be useful? Alternative methods (human, simple rules) aren’t either. Perfect can be the enemy of good enough. Just being pragmatic here.

Aside from seemingly being 100% AI-generated, this article makes a really spurious use of Godel's argument, which I think is best exemplified by the following passage near the end:

"These four threads share a common ancestor in what Gödel proved in 1931, and Turing sharpened in 1936. Rule-based systems cannot fully account for themselves. A system cannot certify its own trustworthiness. A learning framework cannot determine its own boundaries. A safety strategy cannot verify its own completeness.

None of this is softened by the fact that a neural network feels organic rather than rule-like. A model’s weights are numbers, and its training is arithmetic, all of it running on von Neumann’s realisation of Turing’s imaginary device. AI is not adjacent to this mathematics. AI is made of it.

The AI industry, understandably, would rather not dwell on this. "

This is a complete non-sequitur. Godel's argument isn't even that profound: it just says that a system of axioms good enough to embed standard natural number arithmetic must be independent of a certain constructed sentence, i.e., it will run the same whether that sentence is true or false and you can't tell from its axioms which of these two options is in effect. While that sucks for philosophers, it doesn't make mathematics less useful, less dependable, or less correct in a practical sense. It has no practical implications to anything that the AI industry is promising today.

This is a fantastic article with lots of interesting questions raised between the halting problem and applications of AI.

The MRI example is very interesting - add a bit of noise and the crisp results fall apart. But we know we can carve out some determinism by orchestrating around LLM (validation loops) but they are only as good as the coverage of validation and the fidelity of expectations.

Which raises a fundamental question: where is the line between an effective harness and a broken one?

To put it in halting problem terms, if we have an outside program that checks the internal program for halting, we know we will capture some number of previously incatchable halting problems. How can we quantify this? We know there is a class of halts we can catch and prevent, but there will always be more complex ones that escape us.

In the real world, knowing the task is impossible doesn't impact the value of reducing the problem. More importantly, knowing which types of halting problems can be fully captured and which ones are intractable. Agent orchestration could directly benefit from layering a framework over this fuzzy space of knowableness.

Turing proved that no TM can determine whether all TMs halt ... not that no TM can determine whether some specific TM halts ... the difference a common misunderstanding of the proof. Analogously, while we can't prove that no AI is or isn't harmful, we can prove that certain AIs are or aren't harmful.

> The greatest logician since Aristotle

Not to diminish Gödel's work, but the greatest logician since Aristotle was clearly Gottlob Frege, the inventor of modern predicate logic.

This wall of slop is just a long, boring ad.

> We help companies make sense of technology and build lasting improvements to their operations.

Could it possibly be any more meaningless? I could help make sense of words and build lasting improvements to drivel.

Is it just me or does this article have a lot of LLM-isms?

I wrote this partly because nobody seems to know about Gödel who is arguably a more important figure than Turing.

The piece follows four threads where formal limits show up in AI practice today: learnable problems that mathematics cannot sort, neural networks that exist but cannot be trained, self-improving systems that dropped their safety proofs for benchmark scores, and the fact that “will this AI cause harm” is, mathematically, an unanswerable question.

The piece is long and the math is dense. I’m curious whether people see the connection as tight or as overextended—whether Gödel’s structural limits actually do constrain what we’re doing now, or whether I’m collapsing categories that should stay separate.