In the last years of his life, Kurt Gödel starved himself to death. Convinced that someone was poisoning his food, he ate only what his wife Adele had tasted first. When she was hospitalised after a stroke in late 1977, he stopped eating altogether. He died in Princeton Hospital on January 14th 1978, weighing 29 kilograms. The death certificate read “malnutrition and wasting from neglect caused by personality disturbance.” The man widely called the greatest logician since Aristotle, who had proved that mathematics itself contained truths it could never reach, was killed by a distorted inner logic he could not escape.
Outside mathematics, few people know his name. Einstein did. The two were faculty at Princeton’s Institute for Advanced Study from the 1940s onward, and Einstein, by then ageing and isolated from the mainstream of physics, told colleagues that he went to his office “just to have the privilege of walking home with Kurt Gödel.” They made an odd pair on the Princeton sidewalks, Einstein rumpled and laughing, Gödel dapper in a white linen suit, talking animatedly in German on their daily walk to and from the Institute. John von Neumann, who cancelled an entire lecture series on David Hilbert’s programme after reading Gödel’s 1931 paper, called his work “singular and monumental, a landmark which will remain visible far in space and time.”
So what did Gödel prove, and why does it matter now, in the middle of an AI boom that is spending trillions of dollars, much of it resting on the assumption that intelligence is a scaling problem?
What incompleteness means
Put simply, Gödel proved that mathematics cannot fully explain itself. The longer version requires a little patience. In 1900, the German mathematician David Hilbert challenged the field to build what amounted to a perfect machine for mathematics. Start with a set of basic rules (called axioms), things so obviously true they need no argument, and then derive every mathematical truth from those rules, step by mechanical step. If you could do that, mathematics would be complete, meaning every true statement would be provable, consistent, and free of contradictions. You could hand the whole enterprise over to a clerk who follows instructions. This was Hilbert’s programme, and for three decades it was the organising ambition of the field. Then, in 1931, at the age of 25, Gödel demolished it in one stroke.
Gödel’s first incompleteness theorem proved that any set of rules powerful enough to handle basic arithmetic will contain true statements it cannot prove, not because the rules were poorly chosen, but as a structural feature of rule-based systems themselves.
His trick was to construct a mathematical sentence that refers to itself. Consider the sentence, “This sentence has no proof.” Gödel’s technical feat, the part that fills his 1931 paper, was to build this sentence from pure arithmetic, by encoding statements about numbers as numbers themselves. It is not English smuggled into maths. It is pure maths. There are only two possibilities. Either the system can prove it, or it cannot.
If the system can prove “This sentence has no proof,” there is an immediate problem. We have just proved a sentence that claims to have no proof. A system that proves false things is contradictory, and contradictions in mathematics are fatal. Once you allow a single one, you can use it to prove anything, including that 1 equals 2. The system becomes useless.
If the system cannot prove “This sentence has no proof,” there is a different problem. The sentence said it had no proof, and it turns out to be right. It is a true statement. But the system has no way to prove it. So we have a truth the system cannot reach, which means Hilbert’s rulebook has a blind spot.
Any sensible mathematical system would rather have blind spots than contradictions. So the sentence (logicians call it a Gödel sentence) is true but unprovable, and Hilbert’s dream of a rulebook that can prove every true thing was dead.
Logicians would insist on a clarification at this point that the layperson can probably skip. When mathematicians write down rules for the numbers (the axioms), you'd assume those rules describe exactly one thing: the normal numbers, 0, 1, 2, 3, and so on forever. But they don't. The very same rules also accidentally fit some other, weirder number systems that nobody was trying to describe. These weird systems contain all the normal numbers, and then extra “infinite” numbers bolted on past the end. Logicians call these the nonstandard systems. Think of them as impostors: they obey every rule you wrote, so the rules can't kick them out, even though they aren't what you meant.
Here's an everyday version. Suppose you describe your friend as “tall, dark-haired, lives in London.” You meant Sarah. But that description also fits thousands of other people. Your words didn't uniquely capture Sarah. The number axioms have the same problem: they were meant to describe the normal numbers, but they also fit the impostor systems.
The crucial part is what “provable” actually means. In logic, to prove something from your rules means it has to come out true in every system those rules fit, not just the one you had in mind. That's the catch. If a statement is true in the normal numbers but false in even one impostor system, then it cannot be proved, because proof demands agreement across all of them.
Gödel's sentence is exactly such a statement. In the normal numbers, it's true. But in some of the impostor systems, it's false. The systems disagree about it. And because they disagree, no proof can exist. That disagreement isn't a bug in Gödel's argument; it's the reason the sentence is unprovable in the first place. The split between the normal numbers and the impostors is precisely what lets the sentence dodge proof forever.
Gödel’s second theorem twisted the knife. It showed that no set of mathematical rules can prove, using only its own rules, that it is free of contradictions. If you want to check whether your system is trustworthy, you always need a bigger system to do the checking, and that bigger system inherits the same limitation. Turtles all the way down.
This is not mysticism, nor is it a claim about consciousness or creativity. It is a precise result about rule-based systems, the kind of systems that all software, including AI, is built from. That is what makes it relevant today.
The failed dream that built the computer
Hilbert had asked for one more thing, and Gödel’s paper left it wounded rather than dead. Alongside completeness and consistency, he wanted decidability, a mechanical method that could, in a finite number of steps, determine whether any mathematical statement follows from the rules. No genius required: crank the handle and read the verdict.
In 1936, a 23-year-old Cambridge fellow named Alan Turing killed that too. To prove that no mechanical method could exist, he first had to pin down what “mechanical method” meant, which nobody had done before. His answer was an imaginary device, a paper tape and a head that moves along it, reading and writing symbols according to a fixed table of rules. Anything a human clerk could work out by rote, this device could also work out.
Then he showed the device has a blind spot of its own. Imagine a fortune-teller who is never wrong, and a stubborn customer determined to sabotage every forecast. “You will leave by the door.” He climbs out the window. “You will take the window.” He strolls out the door. She is not bad at her job. The job is impossible because her prediction feeds back into the very behaviour it is trying to predict.
Turing turned that scene into code. The checker plays the fortune-teller. It is a program whose job is to read any other program the way you might read a recipe, then predict its fate. Either “this one finishes” or “this one grinds on forever.”
The saboteur plays the stubborn customer. It is a short program with a copy of the checker tucked inside, plus one standing rule. Ask the checker what I am predicted to do, then do the opposite. If the prediction is that it finishes, it deliberately loops forever. If the prediction is that it runs forever, it stops dead.
So what does the checker predict for the saboteur? “Finishes” is wrong, because the saboteur hears that and loops. “Grinds on forever” is wrong, because the saboteur hears that and stops.
The saboteur is assembled entirely from the checker’s own parts, which makes it inevitable rather than a fluke. Build a perfect checker, and you have, in the same afternoon, built the plans for the thing that breaks it. A perfect checker is therefore a contradiction in terms.
Two boundaries stop this result from proving too much. First, it concerns the universal case. Turing showed that no single checker can deliver a correct verdict on every program. Any particular program may still be provably fine, and many are. Static analysers and type checkers pass useful judgement on ordinary code all day, and whole operating system kernels have been formally verified.
Second, the proof needs unbounded memory. A physical computer is a finite-state machine, so in principle its fate could be settled by enumerating its states. In practice, the state count for any interesting program dwarfs the number of atoms in the observable universe, which turns the question from impossible into unaffordable. Keep that distinction in hand, because it returns when the subject is AI safety. What cannot exist at any price is the checker that is never wrong about anything. That is the halting problem, Gödel’s self-referential sentence rebuilt from machinery, a machine forced to ask a question about itself.
To show what machines cannot do, Turing had to invent the machine. His imaginary device is the theoretical blueprint of the general-purpose computer, a single machine that can run any program you feed it as data. Nine years later, John von Neumann, who knew Turing’s paper well and admired it, wrote the First Draft of a Report on the EDVAC, which is, in logical terms, Turing’s universal machine rendered in vacuum tubes. Essentially every computer built since follows that design. The laptop on your desk and the datacentre GPU training the next frontier model are, once the engineering is stripped away, the same device from a 1936 logic paper.
Gödel himself thought Turing had done him a favour. It was Turing’s definition of a mechanical procedure, he wrote, that made a “precise and unquestionably adequate” general version of his own theorems possible. And the machine in the theorem turned out to be the thing every business now runs on, born as a stepping stone in a proof about what it could never do.
The Gödel machine and the guarantee that vanished
Once you have a machine that can run any program, another question is whether it can improve itself autonomously. In 2003, the German computer scientist Jürgen Schmidhuber proposed a thought experiment he called the Gödel machine. It was an AI agent designed to rewrite its own code, with one ironclad constraint. It would change itself only when it could first prove, with mathematical certainty, that the change would make it better. Not “test and see.” Prove it, as you would a theorem, before running the new version. No proof, no rewrite.
But nobody ever built one. To prove that a code change will improve future performance, you need to search through all possible mathematical arguments that could establish that fact. For any interesting problem, the number of candidate proofs is so astronomically large that the search would take longer than any improvement could ever be worth. It is the computational equivalent of insisting on a signed certificate from every possible future before crossing the road. The Gödel machine was provably optimal but completely impractical.
In May 2025, the Japanese AI lab Sakana released a system called the Darwin Gödel Machine. It retained the self-improvement loop but dropped the proof requirement. Instead of proving that a code change would help, the Darwin Gödel Machine proposes changes using a large language model, tests them against SWE-bench (a benchmark that scores whether an AI can fix real bugs in real software), and keeps what works. The name still invokes Gödel, but the mechanism is Darwinian. Natural selection, not formal proof. Fitness measured by benchmark scores, not mathematical certainty.
Judged purely on the scoreboard, it delivered. The system improved its SWE-bench score from 20% to 50% through autonomous self-modification. It developed emergent behaviours, such as patch validation and error memory, that no one had designed.
Schmidhuber’s original machine, though, had exactly one property that made it safe by construction: the proof. Every modification was guaranteed to be an improvement before it ran. The Darwin Gödel Machine replaced that guarantee with something weaker: passing the benchmarks. The difference between “provably better” and “scored higher on the benchmark test” is the difference between an aircraft type certified against a spec and one that simply hasn’t crashed yet.
This is, compressed into one system’s evolution, the trajectory of AI safety. The formal guarantee was too expensive, so the industry replaced it with empirical validation. “Self-improving” went from a mathematical statement about proof-carrying code to a softer description of an agent that rewrites itself and checks whether the benchmarks improve. Gödel was gone.
Things mathematics cannot learn
Some questions in the mathematics of machine learning are unanswerable. In 2019, Shai Ben-David and colleagues published a paper in Nature Machine Intelligence under the understated but devastating title “Learnability can be undecidable.” They took a straightforward question, “given this type of problem, can a machine learn to solve it?”, and proved that the deepest rules of mathematics cannot always settle it. The answer is neither yes nor no. It is silence.
The word “learnable” has an exact meaning here. A machine studies a sample and produces a rule, which it then applies to data it has never seen. That is the basis of pretty much every model we use. For any given type of problem, learning theory asks whether some sample size can guarantee the rule will work. If such a guarantee exists, the problem is learnable. If none does, it is not. A simple question with two answers, and every type of problem is supposed to get one.
Ben-David's team asked it about a mundane task: choosing which adverts to show a website's visitors from a sample of past ones. Learnable or not?
The answer, in their framework, depends on how many different kinds of visitor there could possibly be. That pool is not the eight billion people alive today. The model reduces each visitor to a profile of measurements, and measurements can vary without limit. A visitor might linger on a page for three seconds, or for a shade over three, and between any two profiles there is always room for a third. The pool of possibilities has no end.
That arrangement, a finite sample making predictions about an endless pool, sits under almost every AI product on the market, advertising included. Training data is always finite. The world a system is released into is not. Ben-David's question is whether that leap can ever come with a guarantee, and everything turns on how big the infinity is.
That sounds like it must have an answer. It does not. Georg Cantor proved in the 1870s that infinity comes in sizes. The whole numbers form one infinity. The points on a line form a strictly bigger one, and the proof is surprisingly simple. Try to pair every whole number with a point on the line, and Cantor showed you will always miss some, no matter how clever the pairing. Both collections are endless, yet one permanently outruns the other. The continuum hypothesis asks a follow-up so obvious it would occur to a child. Is there any size of infinity between those two?
Gödel proved in 1940 that the standard rules of mathematics can never prove the answer is yes. Paul Cohen proved in 1963, using a technique he invented for the purpose, that they can never prove it is no. His proof is dense, and we are already deep enough in theoretical mathematics.
The upshot is that no cleverer generation is coming to settle this one. The rules of mathematics contain no answer. Take every rule of arithmetic and logic we have and follow them as far as they go, in whatever direction you like. You will never reach yes, and you will never reach no. The question is open in both directions, permanently.
Whether the advertising problem is learnable depends on the size of that infinity. The size of that infinity is a question mathematics cannot answer. So whether the advertising problem is learnable is also a question mathematics cannot answer. The strange silence at the very bottom of mathematics travels up the chain and surfaces as a question about showing adverts to shoppers.
Two objections surfaced almost as soon as other mathematicians looked hard at the paper.
The first is about what counts as a learner. A learner here is just the rule a system follows to turn examples into predictions. Ben-David's framework allows that rule to be any mathematical function whatsoever, including ones no computer could ever evaluate. In the cases where the undecidability appears, the rule doing the learning is exactly one of those uncomputable phantoms. It leans on a particular way of lining up all the real numbers, an object the axioms promise exists but give no recipe for building. The rule exists on paper, but no program could carry it out.
The second follows from the first. Insist that a learner be a real algorithm, something that runs on an actual machine, and the whole paradox drains away. Ben-David's own team showed this the following year: once the learner has to be a working program, learnability becomes an ordinary question with an ordinary answer. The silence at the bottom of mathematics never reaches the code. It stays out in the realm of functions nobody could ever build.
So no deployed system is endangered, but the result is no sleight of hand either. Something real did break. It just wasn't a product. What broke was the promise that learning theory could sort every problem into neat buckets: learnable or not. Ben-David found a problem it can never sort. Not for want of better mathematicians, a problem where the sorting itself is impossible. The University of Waterloo, Ben-David's institution, described the result as “important and almost troubling.”
The neural network that exists and cannot be built
A complementary result, published in 2022, is narrower and stranger. Training a neural network is, at bottom, an exercise in trial and error. You show the network examples, measure how wrong its answers are, then nudge its millions of internal settings to make them slightly less wrong. Repeat this billions of times, and often the network converges on something remarkably good. The Cambridge mathematician Matthew Colbrook and colleagues showed in a 2022 paper in PNAS that this process has a hard boundary nobody expected.
The boundary appeared in medical imaging. An MRI scanner does not take a photograph. It collects measurements to keep patients in the incredibly claustrophobic machine for minutes rather than hours, so it collects far fewer than a complete image requires. Software has to rebuild the full picture from the partial data. Neural networks became the favoured tool for this reconstruction because they perform it faster and more accurately than older mathematical methods.
Then researchers started probing the results and found something unnerving. Nudge the input slightly, with a trace of noise or a small movement by the patient, and the output could change out of all proportion. Sometimes the rebuilt scan came back looking perfect but wrong, showing details that were never in the body. Worse, it is a failure that does not look like a failure. A blurry image warns you. A crisp fabricated one does not.
A demonstration of capability may show nothing is amiss, not because anyone is cheating. A demo runs the network on typical inputs, the kind it was trained on, where it genuinely performs well. The failures live in the near-misses, a typical input plus a whisker of noise. Near-misses are endless, and a demo can show only a handful of scenarios. The demo is honest, and the danger lies exactly where it cannot be seen.
The natural presumptive diagnosis is undertraining. Feed it more scans and buy a bigger model, and the wobble will surely iron itself out. That hope is what Colbrook’s theorem takes off the table. What the paper proved has two halves. First, for certain reconstruction problems, a network that is both accurate and stable exists. Somewhere in the space of all possible settings sits a configuration immune to the wobble. Second, no training procedure can find it. Not the ones we have. Not any. None at all, ever.
The second half is what kills the more-data hope. A training procedure is itself a program, a step-by-step recipe running on the machine Turing described, and the proof covers every recipe there could ever be. More data does not change that. Data is what you feed a recipe, and the theorem is about the recipes. It is like knowing a winning lottery ticket is in a barrel whilst simultaneously holding a proof that no way of drawing from the barrel will ever pull it out. The ticket is real. The searching is futile.
As Colbrook put it, the paradox Turing and Gödel identified has now been “brought forward into the world of AI”, and for certain problems the required algorithms simply cannot exist.
For the overwhelming majority of real-world problems, training works. But there is no general way to tell in advance which problems will defeat us, and the assumption that enough data and compute will always get us over the line is, in certain corners of the problem space, provably false.
The machine you cannot contain
The most provocative extension of Gödel’s legacy into AI concerns a question that sounds simple. Can we guarantee that a sufficiently powerful AI will not cause harm?
In 2021, Manuel Alfonseca and colleagues published a paper in the Journal of Artificial Intelligence Research arguing that, for a general-purpose superintelligent system, the answer is provably no. Their argument leans on the halting problem, the impossibility Turing established on his way to inventing the computer. You can check specific programs for specific bugs. What you cannot build is the universal checker, the one that works for any program in any situation.
Alfonseca’s team showed that asking “will this AI harm humans?” is, for a fully general system, the same type of question as asking “will this program halt?” Both require predicting the complete future behaviour of a system from its current state. To guarantee a system will never cause harm, you would need to trace every possible sequence of actions it could take and confirm that none is harmful. That is the halting problem in different clothes, and Turing proved that this class of prediction is impossible to guarantee. You cannot build a general-purpose AI safety monitor for the same reason you cannot build a general-purpose program-behaviour predictor.
The scope of that impossibility deserves the same care as Turing’s original. What cannot exist is the universal judge, one procedure that delivers a correct safety verdict for every possible system and every possible input. Specific systems doing bounded work in bounded settings can be certified, and safety engineering does exactly this, one component at a time. Wrapping a monitor around an agent catches genuine failures and is worth every penny.
But each monitor is itself a program with the same blind spot, so layered checks buy coverage, but never closure. And since a physical machine has finite memory, its behaviour is in principle a finite question, merely one whose size defeats any conceivable budget. For a bounded system, the wall is cost. For the unboundedly general system Alfonseca’s team modelled, the wall is mathematics.
The authors went further, showing that we may not even be able to recognise when a superintelligent system has arrived, because deciding whether a machine is smarter than a human falls into the same class of unanswerable questions. The argument is grounded rather than speculative, though it assumes a generality no AI system possesses today. Nothing currently available can handle any possible input the way a true Turing machine can.
What it establishes still matters, though. Certain safety guarantees are not engineering problems awaiting a sufficiently clever solution. They are mathematical impossibilities, like trying to square the circle or list every real number between 0 and 1. The safety community can build better guardrails and better kill switches. What it cannot build, given the computational framework we share, is a system that certifies another system as unconditionally safe.
What Gödel would recognise
These four threads are cousins rather than corollaries of a single theorem. Incompleteness limits what rule systems can prove about themselves. The halting problem limits what programs can decide about programs. Colbrook’s result limits what algorithms can find. And the Darwin Gödel Machine story records a design retreat, a choice rather than a law of nature. What joins them is that in each case a formal guarantee is either unavailable in principle or unaffordable in practice, and the work must proceed anyway on empirical confidence.
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.
Nor is any of it an argument that machines cannot think. These limits bind every formal reasoner, and on the standard understanding of physics, that includes the three pounds of wet machinery reading this sentence. You cannot prove your own consistency either. Humans invent, reason, and get things done inside exactly the same boundaries; evidence that the boundaries are no bar to intelligence. Gödel constrains what can be guaranteed about a mind, human or artificial. He says nothing about what a mind can do.
A fair objection is that the AI industry never promised mathematical proof, and empirical validation is how almost everything gets built. Aircraft are tested, drugs are trialled, and nobody demands a theorem before boarding a plane. All true, and for the overwhelming majority of applications, the limits in this piece never come up. Your chatbot will not encounter the continuum hypothesis when summarising a report.
But the objection undersells what the mathematics settles. Testing regimes for aircraft rest on decades of physics that says how materials behave between the test points. For a system that rewrites itself, or one deployed against inputs no test set anticipated, no such interpolating theory exists, and the results above show parts of it never will.
That turns safety from a verification problem into a pricing problem. If certainty is permanently off the table, the question becomes how much assurance a given deployment needs, what it costs to obtain, and who bears the residual risk when that assurance runs out. At present, the industry is a long way from answering those questions explicitly. “Passed the evals” blurs into “proven safe”.
Einstein’s eccentric walking companion saw the underlying structure before anyone else. Formal systems cannot fully certify themselves. That was a logician’s problem in 1931. It became an engineer’s problem when Turing turned the proof into a machine. It is now a commercial problem because the machines carry trillions of dollars in expectation, and expectation is reaching for guarantees that the mathematics declines to issue. Guarantees generated by systems that cannot check themselves any more than Gödel’s own warped internal logic could. He died trapped inside it.
I am a partner in Better than Good. We help smaller companies build tools and processes using machine learning and artificial intelligence that make lasting improvements to their operations. Talk to us today: https://betterthangood.xyz/#contact