Kurzweil Scorecard: The Uncomputable Fell to a Machine. The Next One Won’t Fall to Anyone.

In July 2024, an international band of hobbyists and one anonymous prover known only as “mxdys” finished a piece of mathematics that no human will ever do by hand. They pinned down the exact value of the fifth busy beaver number — BB(5) = 47,176,870 — by having a computer inspect roughly 16.7 trillion candidate Turing machines and then having a second computer check the proof, line by line, in the Coq proof assistant, until every non-halting machine carried a machine-verified certificate of eternal life.

The busy beaver function is the textbook example of a problem that is formally uncomputable: no algorithm can compute it in general, because it grows faster than any computable function can. And yet a machine-driven effort settled one of its values with total rigor — an instance of a formally unsolvable problem, cracked by computers doing what no unaided mind can.

That is almost word-for-word a bet Ray Kurzweil placed twenty years ago. And in the same breath, the busy beaver hunt validated a second, more careful thing he said — that when the truly unsolvable arrives, neither the human nor the machine gets to be the hero.

The predictions

In the criticism-and-rebuttal chapters of The Singularity Is Near (2005), Kurzweil took on the oldest objection to strong AI: the limits of computation. Gödel, Turing, and Church proved there are problems no machine can solve. Doesn’t that cap what an artificial mind can ever do?

Kurzweil’s answer came in three moves. First, a leveling claim: humans are no more capable than machines of universally solving formally unsolvable problems, though both can make educated guesses in some cases (The Singularity Is Near, ch. “A Panoply of Criticisms”). The wall of undecidability, he argued, is not a wall that only machines run into. It stops us too.

Second, a forecast: computers will prove more capable than humans at solving some instances of formally unsolvable problems, because they can track and manipulate far more complex numbers and search spaces (ch. “The Criticism from the Church-Turing Thesis”). The names attached to this prediction in our records are telling — Alan Turing, and Tibor Radó, the mathematician who invented the busy beaver game in 1962.

Third, the payoff: the Church-Turing thesis does not prevent machines from emulating human intelligence, because heuristic and guess-based methods are also algorithmic (ch. “A Panoply of Criticisms”). Human cleverness, he insisted, is not a magic exemption from computation. It is search plus good guessing — and guessing can be programmed.

Three claims, made when the state of the art in “machine reasoning” was a chess engine. Here is where each stands.

Where we actually are

The machine did what the human couldn’t. Start with the middle prediction, the one that came due most literally. BB(5) = 47,176,870 was conjectured in 1990, when Heiner Marxen and Jürgen Buntrock found a five-state machine that runs exactly that many steps and halts. Conjecturing was the easy part. Proving no other five-state machine runs even one step longer meant deciding, for each of millions of surviving machines, whether it halts or loops forever — and halting is the undecidable problem, with no general method. The bbchallenge collaboration got there anyway, machine by machine, closing the last stubborn holdouts with hand-built “deciders” whose correctness was itself verified in Coq. Scott Aaronson, whose 2020 survey “The Busy Beaver Frontier” set the agenda for the effort, called it a milestone generations of pencil-and-paper hobbyists had failed to reach.

This is the cleanest confirmation in the scorecard: a formally uncomputable problem, one instance settled decisively, by computers tracking a search space no human could hold in their head. Kurzweil said this would happen. It happened, and a proof assistant signed off on it.

Then came the Antihydra. The leveling claim — that machines don’t get to be universally better, because the wall stops them too — arrived on almost the same day. In June 2024, hunters searching six-state machines found one they named Antihydra. It runs forever if and only if a Collatz-like conjecture holds: iterate a certain doubling map from a starting value, and the odd outcomes never run more than twice ahead of the even ones. Nobody knows if that’s true; it is a cousin of the Collatz conjecture, which has resisted every mathematician alive. As Quanta reported this past August, “slaying the Antihydra and its brethren will require conceptual breakthroughs in pure mathematics” — not more compute. The lower bound on BB(6) now exceeds a tower of exponents so tall, in pentation notation 2↑↑↑5, that Quanta noted “even this more compact notation no longer fits in the universe.”

Push one more state and it gets worse in a way that indicts human mathematics directly. Adam Yedidia and Aaronson built a Turing machine — originally 7,910 states, later whittled down to 643 by July 2024 — whose halting behavior cannot be decided within ZFC, the standard axioms underpinning essentially all of modern mathematics. If the machine’s fate is independent of ZFC, no proof in ordinary mathematics settles it. Not a machine proof. Not a human proof. The wall Kurzweil described is real, and exactly as high for us as for the silicon. Prediction one holds — verified by the same hunt that verified prediction two.

Heuristics turned out to be algorithmic after all. The third claim was the boldest and least testable in 2005: that human-style guessing is nothing but algorithm, so the Church-Turing thesis is no barrier to a machine emulating a mind. For nearly two decades this stayed philosophy. Then large language models turned it into an engineering result. In The Singularity Is Nearer (2024), Kurzweil retells the moment scholar Amanda Askell fed GPT-3 the setup of John Searle’s Chinese room argument. The model replied that a translation program “does not explain understanding any more than a cookbook explains a meal” — a metaphor, Kurzweil notes, that “had never appeared anywhere before.” His rejoinder: “because those statistics are synthesized from the combined creative output of millions of humans, the AI attains genuine creativity of its own.”

The strongest evidence isn’t chat, though — it’s proof. DeepMind’s AlphaProof scored 28 of 42 points at the 2024 International Mathematical Olympiad, silver-medal territory and one point shy of gold, solving the competition’s hardest problem — one that only five human contestants cracked. A year later, a Deep Think version reached the gold-medal threshold. AlphaProof is built from exactly the guess-and-search machinery Kurzweil described: a neural network proposing moves, wrapped around the AlphaZero tree-search algorithm, generating candidate proofs in the formal language Lean and keeping only the ones the Lean kernel certifies. Educated guessing, made algorithmic, verified by a machine — good enough to medal against the best young mathematicians on Earth.

The mechanism is patented. US 10,867,242, granted to DeepMind in 2020, claims a system that maintains a “state tree” of an environment — each node a state the agent has reached, each edge an action it took — with a value neural network scoring how good each state is. That is the AlphaZero engine AlphaProof later pointed at mathematics instead of Go. In our records, patents pairing large language models with explicit “reasoning” climbed from one filing in 2023 to twelve so far in 2026; papers on neural theorem proving rose from 45 in 2018 to 319 already this year. The guess-based methods Kurzweil bet were “also algorithmic” are now a research industry with their own filing curve.

The scorecard

What Kurzweil missed (and what he nailed)

The pattern in this batch is unusual: Kurzweil got the philosophy exactly right and left the mechanism blank — and reality filled the blank with something better than he could have specified.

He was right that undecidability is symmetric. The romantic idea that human intuition leaps over the barriers that trap machines took a direct hit from the busy beaver hunt: the Antihydra and the ZFC-independent machine are walls for everyone. He was right that a machine could out-reach a human on a specific uncomputable instance — BB(5) is that instance, now signed in Coq. And he was right, most improbably, that “educated guessing” is not a human birthright but an algorithm waiting to be written.

That is the recurring shape of a good Kurzweil call: the direction is uncanny, the vehicle is a surprise. He forecast that heuristics would prove algorithmic. He did not forecast Lean, or AlphaZero, or a language model quoting a cookbook back at John Searle. The destination was on the map. The road hadn’t been built yet.

One caution keeps the scorecard honest. BB(5) is a single instance, not the function; the busy beaver stays uncomputable in general, and always will. And “emulating intelligence” on math-olympiad problems, however impressive, is not the general human-level mind Kurzweil places at 2029. These predictions were about the limits argument — whether computation theory forbids strong AI — not the timeline to strong AI itself. On that narrow question, the critics who wielded Gödel and Turing as a stop sign have quietly lost. The machine went past the sign. So, at the same intersection, did we — and there the road ends for both.

Method note

We track Kurzweil’s 2005 predictions against live evidence: roughly nine million patents, several hundred million scientific papers, and the public record of what got built and proven. For this batch we counted the rise of neural theorem-proving research and language-model reasoning filings to establish the trend, then read the actual claims of the DeepMind tree-search patent and the findings behind the 2024 busy beaver proof, the Antihydra machine, and the ZFC-independent Turing machine. Quotations from Kurzweil are drawn from The Singularity Is Near (2005) and The Singularity Is Nearer (2024). Where a result mattered — Aaronson’s account of BB(5), Quanta’s reporting on the BB(6) frontier, DeepMind’s IMO results — we went to the source rather than resting on counts.