On August 10, 2026, Anthropic announced a mathematical breakthrough. Using an unreleased research version of Claude, they raised the lower bound on the proportion of nontrivial zeros of the Riemann zeta function lying on the critical line from 41.6% to 67.2%. Seeing this number, your first reaction might be: is AI about to crack the Riemann Hypothesis? Not quite. What’s being discussed here is the proportion of nontrivial zeros of the Riemann zeta function, whereas the Riemann Hypothesis requires 100% of the zeros to lie on the critical line. Anthropic itself made it clear in their post that this technique cannot reach a proof of the Riemann Hypothesis.
What really caught my eye were the engineering details extracted from the published materials. Across two Claude Code sessions, a total of 31M output tokens were consumed. The second round coordinated about 60 subagents, ran 2,400 shell commands, wrote hundreds of Python scripts, and downloaded 54 arXiv papers. All 650 ideas proposed in the first round actually failed completely. What was ultimately delivered to humans was an ~35-page paper and a Lean formalization. Doing the math, the vast majority of these 31M output tokens went into searching for viable routes, while only a tiny fraction at the end was used to actually write the paper.
This is precisely what I think is most worth breaking down. When people discuss AI doing mathematics, attention mostly stays on the results: how much the numbers improved, whether the proof is correct, and how far we are from the Riemann Hypothesis. But what’s truly interesting about this release is how those 31M output tokens were spent: how the system searched through unknown routes, how it utilized failure information, and how it separated search and verification into two phases. This article is about that process, as well as a deeper bottleneck it exposes.
Let me start with the difference between search and sampling. Given 31M output tokens to do mathematics, the most obvious approach is to have the model generate hundreds of candidate proofs and use a scorer to pick the most promising one. But this logic quickly runs into a brick wall on complex mathematical problems. If you don’t shrink the search space based on previous results, even sampling ten thousand times is just repeatedly rolling the dice within the same probability pool.
Anthropic’s approach here is much more like engineering, setting kill criteria similar to test-driven early fail for each route. After each route runs, the subagent returns a post-mortem report: which premise killed this path, which local derivations still hold, and what new evidence would be required to reopen it. Equipped with this feedback, the system can revoke compute budget from dead-end routes and reallocate it to unexplored directions. Human mathematicians tackling hard problems actually follow a similar rhythm—constantly testing whether conditions are too restrictive, whether a certain transformation collapses at the boundary, or how far things can be pushed by stepping down the objective a notch. With every resolved point of confusion, the feasible space tightens by another layer.
The public materials mention an interesting instance of hostile review. Before finalizing the ultimate route, the system dispatched three mutually isolated subagents specifically to attack the proof in the draft. One reviewer actually caught a hidden mathematical error: the mass matrix of the test system in the draft was built on a flawed premise, leaving a real gap in the associated derivations. Crucially, this subagent didn’t just point out which assumption failed; it directly provided a repair plan, giving the search direction an actionable update.
However, a prominent risk remains here. Ultimately, this sense of direction stems from the same unreleased Claude model family. Multi-agent parallelism helps reduce accidental oversight in individual reasoning threads, but since their underlying knowledge structure is identical, they can easily overlook shared cognitive blind spots together. Independent cross-model-family review was not fully implemented this time, leaving this correlation risk embedded in the verification chain of the entire system.
Ultimately, the prerequisite for shrinking the search space is understanding what the system is actually searching for. When we usually write code, searching often boils down to tuning parameters within a given framework. But in mathematics, search is far richer. The system must not only figure out how to piece together existing tools, but also test how intermediate propositions can be rewritten, which quantity can yield a tighter lower bound, which additional assumption blocks unconditional proofs, and even design numerical experiments with the highest kill potential to eliminate blind spots quickly. The toolkit Claude pulled in this time included the Weil explicit formula, Montgomery pair correlation, and Bombieri’s work on quadratic forms.
The most key breakthrough this time was actually adopting a fresh perspective on the objects involved. Previous routes demanded that the relevant mathematical quantities be term-by-term positive, causing derivations to easily stall. Claude changed tack: instead of strictly requiring positivity across the entire structure, it turned to count how many positive directions were actually contained within. As long as there are enough usable positive indicators, the conclusion holds. This single shift instantly relaxed the rigid constraints of the original routes—far more effective than mechanically crunching a few extra steps down the old formulas.
This broad exploration demonstrates a key engineering advantage: the trial-and-error cost for low-probability routes is drastically reduced. Human mathematicians, limited by energy and community consensus, rarely spend months hammering away at directions widely deemed hopeless. But for a model, scanning these tail routes is merely a matter of compute allocation. OpenAI’s GPT-5 previously exhibited a similar pattern on the Erdős unit distance problem, where number theorist Arul Shankar noted that the model was remarkably willing to try paths that the community considered extremely low probability.
Even more interesting were the 650 completely failed ideas in the first round. A typical script would simply wipe the slate clean and start over after a failure. But the first round left behind 106 survivors containing partial content, compiled into a ledger. Far from being half-written proofs, this ledger meticulously recorded where each route got stuck, why it failed, which small local conclusions still held up, and what new conditions were required to reopen it. Coming into the second round, the system consulted this ledger first, performing a barrier check on each of the 106 old routes to confirm no gaps were missed before forging new directions. In this way, failure information was transformed into a do-not-repeat list.
Furthermore, these ledger entries served as stepping stones across different routes. The materials record a specific detail: a partial judgment left over from the first round initially seemed completely useless, but 12 hours later was resurrected in an entirely new route, perfectly filling a critical gap. Pushing the lower bound value was likewise accomplished through instance relaying—one subagent first pushed the version to prove 1/2, another parallel run pushed it further to 2/3, and fine-grained optimization finally reached 0.6725. From start to finish, no single instance ran the full distance in one go.
Of course, the public materials currently only reconstruct this single successful path without releasing the full route transition graph. What we can be certain of is that the system indeed recorded and leveraged failure assets, and stepping-stone transfers genuinely occurred. As for whether a more complex cross-route heuristic network formed behind the scenes, there is currently insufficient evidence.
Additionally, discussing the level of breakthrough of this result requires addressing the narrow-box condition. The so-called narrow-box condition assumes that all zeros lie close to the critical line within a narrow strip. Works by scholars Baluyot, Goldston, Suriajaya, and Turnage-Butterbaugh between 2024 and 2026 had actually already reached 67.25% under the narrow-box assumption (arXiv:2501.14545; arXiv:2603.28104). Therefore, this 25.6 percentage point leap cannot be attributed entirely to Claude inventing increments from scratch. Its true substantial contribution was shedding the narrow-box condition entirely, piecing together existing unconditional prime-side inputs with the Weil indefinite form, Sylvester’s inertia law, and rank-trace readouts. As for how historical priority is ultimately assigned, that awaits final confirmation by domain experts.
After the search process finished, producing an ~35-page paper and Lean code, the real test was just beginning. To understand what stage this deliverable has reached, the five-stage acceptance ladder we built when analyzing OpenAI’s ten mathematical advances fits this release perfectly. The five stages are: L1 Candidate Generated (paper or draft exists); L2 Rules Checked (passes hard machine checks such as Lean compilation, sorry-free code, and axiom audits); L3 Intent Aligned (the formalized proposition faithfully expresses the original problem without quiet downgrades); L4 Peers Understood (external experts grasp the core logic and scope of applicability); L5 Community Absorbed (the result enters mainstream literature, and methods are reused in subsequent research).
Anthropic did a very solid job on L2. The Lean repository
fully covers the core asymptotic conclusions of Theorems A–E, with no
sorry placeholders in the proof code; the 33
sorrys used in the trusted challenge to state acceptance
targets do not enter the solution proof. Top-level theorems depend only
on Lean’s three standard axioms. They also used a comparator to run
statement equality checks and kernel replay, and community members even
successfully replayed the build on a fixed commit. Formalized statements
hook directly into Mathlib’s riemannZeta definition rather
than substituting toy functions, ensuring machine checks directly
targeted the core objects of the paper.
However, code coverage here has two noticeable gaps. One is that the effective form mentioned in the paper was not included in the headline statements, and the other is that the reference script used in the paper for 31 SymPy symbolic checks was not included in the frozen repository. While these gaps don’t undermine the main conclusions, they do show that formalization shouldn’t be conflated with Lean thoroughly verifying every single natural language sentence in the paper.
At L3, the line currently holds, though independence is slightly weak. Two mathematicians internal to Anthropic, Alpöge and Furman, conducted an in-depth review and took academic responsibility, even writing an informal note to help peers quickly grasp the main points. However, since both are employed at Anthropic, while intent alignment does have endorsers, publicly auditable review by independent third-party humans remains absent for now.
As for L4, there are currently only early signals. Brian Conrey and Dan Goldston looked over the paper on short notice and provided feedback, but as of about a day after release, there are no public review reports or individual public technical evaluations. The official phrase “examined on short notice” explicitly refers to brief reading, which cannot be directly equated to formal peer review. As for L5, with the release only a day old, community absorption naturally hasn’t happened yet.
Looking at Anthropic’s work alongside OpenAI’s ten advances, its incremental contribution lies entirely at the front end of the acceptance ladder. Back then, OpenAI already had projects touching L4 or even L5—for instance, the proof mechanism for non-sofic groups was quickly picked up by other scholars to construct new objects. Anthropic’s contribution lies in making transparent the search funnel prior to L1, letting us clearly see how 650 failed ideas converged into a final route via kill criteria and failure ledgers. As for how far the result itself can progress on the acceptance ladder, it didn’t set a new record.
Although Anthropic’s result alone did not set new records on the back half of the ladder, comparing these recent representative cases reveals an interesting trend: the bottleneck is shifting from search to absorption. After GPT-5 broke through on the Erdős unit distance problem, several mathematicians spent time organizing and simplifying the model’s raw logic to write a companion paper readable by humans, after which Will Sawin followed up to refine the exponent to . The model produces the discovery first, and humans subsequently spend even more effort digesting it.
After OpenAI released those ten advances, the digestion pace for different topics diverged drastically—some results quickly reached L5, while others remained stuck at L2. Terence Tao’s IEANTN project showcased the same contrast: AI can indeed shrink formalization tasks that used to sit unassigned in the community for weeks down to a few hours, but the proof processes produced by models are overly verbose and unnaturally abstracted. Consequently, human review and refactoring ended up being the most time-consuming part. In Anthropic’s case, the full campaign ran for 54 hours across three calendar days, completing the route search and delivering Lean code, yet a day after release, the mathematical community’s absorption process has barely begun.
Putting these phenomena together, the trend is crystal clear: the speeds of generation and formalization are accelerating rapidly, but the speed of human understanding and absorption remains virtually unchanged. As long as the generation side continues to accelerate, the bottleneck of the entire research system will naturally shift from whether something can be found to whether people can understand and trust it once found.
The role of humans in the research chain is also evolving. People no longer need to perform mechanical grunt work; instead, energy is shifting to several key touchpoints: selecting which problems are worth attacking, closely monitoring whether formalized statements drift from original intents, rewriting awkward AI-generated proofs into human-readable paradigms, and deciding which outputs qualify to be written into the shared knowledge base. All of these tasks lie squarely at the intersections of different systems, while pure code or text generation is rapidly shrinking as a proportion of the overall workflow.
For those of us designing AI systems, the most central decision point along the verification chain is actually: what can be promoted to a shared premise. Drafts written in natural language must first converge into formalized statements where objects, quantifiers, and constants are airtight before being handed over to machines to match proof terms. Without the constraint of formalization, about 60 subagents from the same model family could easily reach a highly correlated, hallucinated consensus within a pile of vague prose. Once this layer is established, Lean can catch the vast majority of logical loopholes at the boundaries of statements and definitions.
Yet formal alignment ultimately still requires human gatekeeping. Lean’s kernel neither knows whether code faithfully conveys the true intent of the paper, nor is it aware that external scholars had already achieved the same constant under the narrow-box condition. Claude did not prove the Riemann Hypothesis this time, and the new lower bound of 67.2% is merely the surface manifestation of this release. The deeper signal is that AI research systems are beginning to perform directional searches on open, complex mathematical problems and compress the tiny handful of successful routes into auditable deliverables. The widening time gap between search and verification is pushing more and more of the cost onto the human side. The next most expensive, hardest-to-scale bottleneck is understanding and verification.