The Verification Oracle Determines the Ceiling: Why Artificial Intelligence Advances Unevenly Across Mathematics, Physics, and Biology

1.1 The observation to be explained

A striking asymmetry emerged over the eighteen months preceding this writing. In mathematics, AI systems progressed from solving five of six International Mathematical Olympiad problems in July 2025 to producing formally verified resolutions of previously open problems, including cases where no prior human literature resolving the problem could be located. Tao's community wiki tracking AI contributions to the Erdős problem database documents this trajectory in unusual detail, and it is one of the few places in AI-for-science where the record is systematic rather than anecdotal.

In physics, the picture is different in kind, not merely in degree. AI has become load-bearing infrastructure — deep reinforcement learning for tokamak magnetic control, neural surrogates replacing expensive transport and heat-flux calculations, disruption predictors running in real time on experimental devices, national platforms coupling AI directly to experimental facilities. These are substantial achievements. But almost none of them are of the form "the system produced a novel physical law and we accepted it." They are of the form "the system produced a fast approximation to something we already knew how to compute, or a control policy whose success is measured by whether the plasma stayed confined."

In biology, the picture is different again. AlphaFold's impact on structural biology is not in dispute; it broadened the set of proteins the field considers tractable, and roughly 40% of new PDB depositions between 2024 and 2025 involved AI-assisted techniques. Agentic systems now generate hypotheses that survive wet-lab validation — FutureHouse's Robin proposing ripasudil for dry age-related macular degeneration, DeepMind's Co-Scientist producing testable hypotheses about bacterial gene transfer that aligned with independently obtained empirical findings. Yet the rate-limiting step in every one of these stories is the same, and it is not the AI. Reagents must be obtained. Cells must grow. Weeks pass.

A tempting explanation is that mathematics is "easier for AI" because it is symbolic and biology is "harder" because it is messy. This explanation does not survive contact with the details. Research mathematics draws on decades of specialist literature and requires constructions that current systems demonstrably cannot produce. Protein structure prediction, by contrast, was solved to near-experimental accuracy for single chains — a problem far more "messy" by any naive metric — while research-level mathematics remained largely out of reach. The naive difficulty ordering is wrong.

1.2 The thesis

We propose instead:

The autonomy an AI system can achieve in a scientific domain is bounded above by the quality of that domain's verification oracle, largely independent of the system's generative capability.

The claim is a ceiling claim, not a floor claim. A strong oracle does not guarantee progress; it permits it. A weak oracle prevents autonomy regardless of how good the generator becomes, because the generator's output cannot be converted into knowledge at a rate faster than the oracle can adjudicate it.

This reframes the central question of AI-for-science. The question is not "how capable is the model?" It is: what is the specification a verification procedure must meet for this domain to admit autonomous discovery, and how far is the current procedure from meeting it? Stated this way, the apparent prohibition — "AI cannot do autonomous biology" — dissolves into a cost structure. Autonomous biology is not forbidden. It is expensive in a specific, nameable currency: oracle latency and oracle completeness. That currency can, in principle, be paid down.

1.3 Scope and epistemic discipline

This paper mixes three kinds of claim, and conflating them would replicate the error it is written to avoid. Claims are therefore tagged throughout as:

• —[E] — Empirical. A documented fact about the world, with a source.
• —[F] — Framework. A definitional or analytical construct proposed here. Not true or false; useful or not.
• —[C] — Conjecture. A substantive claim advanced here that could be wrong and that we specify how to test.

A complete ledger of load-bearing claims, with epistemic status and falsification conditions, appears in Appendix A. Readers who want the argument's honest skeleton should read Appendix A first.

2.1 Definition [F]

For a scientific domain $D$, define the verification oracle $V_D$ as the procedure that maps a candidate claim $c$ to a verdict in $\{\mathrm{a}\mathrm{c}\mathrm{c}\mathrm{e}\mathrm{p}\mathrm{t},\mathrm{r}\mathrm{e}\mathrm{j}\mathrm{e}\mathrm{c}\mathrm{t},\mathrm{\perp }\}$, where $\mathrm{\perp }$ denotes "cannot adjudicate."

Characterise $V_D$ by four parameters:

• —Parameter Symbol Definition
• —Latency $\tau$ Wall-clock time from submission of $c$ to verdict
• —Marginal cost $\kappa$ Resource cost of one additional adjudication
• —Completeness $\gamma$ Fraction of well-formed claims in $D$ for which $V_D(c)\mathrm{\ne }\mathrm{\perp }$
• —Fidelity $\varphi$ $P(\text{verdict correct}\mid \text{verdict}\mathrm{\ne }\mathrm{\perp })$

An ideal oracle has $\tau \to 0$, $\kappa \to 0$, $\gamma \to 1$, $\varphi \to 1$. No real oracle is ideal; the interest lies in how far each domain sits from the ideal and along which axis it fails.

2.2 Why the oracle bounds autonomy [C]

The mechanism is a search argument. A generative system explores a space of candidate claims. Its useful output rate is

where $R_{\mathrm{g}\mathrm{e}\mathrm{n}}$ is the rate of plausible candidate generation and $R_{\mathrm{v}\mathrm{e}\mathrm{r}}\approx \gamma \mathrm{/}\tau$ is the rate at which candidates are adjudicated.

Three consequences follow.

First, the bottleneck is whichever term is smaller. In mathematics, $R_{\mathrm{v}\mathrm{e}\mathrm{r}}$ is enormous — a Lean kernel checks a proof in milliseconds — so $R\approx R_{\mathrm{g}\mathrm{e}\mathrm{n}}$, and improvements to the generator translate directly into improvements in output. In biology, $\tau$ is measured in weeks and $\gamma$ is low, so $R\approx R_{\mathrm{v}\mathrm{e}\mathrm{r}}$, and a tenfold better hypothesis generator produces approximately zero additional validated knowledge per unit time.

Second, and more consequentially, the oracle is what makes self-improvement possible. A system whose outputs are cheaply verified can generate its own training signal. This is the reason mathematics has moved fastest: correct proofs are recognisable as correct without human labour, so synthetic data can be generated and filtered at scale. Where the oracle is expensive, this loop does not close, and the system remains dependent on the fixed supply of human-generated data.

Third, low $\gamma$ produces a distinctive and dangerous failure mode. When an oracle can adjudicate formal correctness but not significance, an optimiser directed at the oracle will produce output that is correct and worthless. This is not hypothetical. Feng et al.'s systematic evaluation of Aletheia against 700 problems from Bloom's Erdős database found that of the responses graded, a substantial fraction were technically valid but mathematically vacuous — the problem statement had been interpreted in a way that did not capture Erdős's intent, often yielding trivial solutions. The formal oracle said "accept." The intent oracle did not exist. We return to this in §6.

2.3 The distinction from difficulty [F]

Oracle quality is orthogonal to problem difficulty. The Riemann Hypothesis has an excellent oracle (a Lean proof would be checkable in seconds) and is extraordinarily difficult. Determining whether a given transcription factor knockout is therapeutically useful in humans is, conceptually, not very difficult — and has a terrible oracle, because the adjudication requires a clinical trial.

This orthogonality is the framework's main claim to non-triviality. It predicts that fields will not order by intuitive difficulty, and they do not.

3.1 Oracle parameters

Formal proof assistants — Lean 4 with Mathlib, Coq, Isabelle — give mathematics an oracle with properties no other empirical science can match:

• —$\tau$: milliseconds to minutes.
• —$\kappa$: negligible; a laptop suffices for most checks.
• —$\gamma$: high but not unity, and this is the interesting caveat. Formalisation is complete for statements that have been formalised. The bottleneck is the translation from informal mathematics into the formal language, and that step remains substantially human — or, increasingly, AI-assisted but human-audited.
• —$\varphi$: essentially unity, conditional on the formal statement faithfully rendering the informal one. The kernel does not make mistakes. The translation does.

The load-bearing observation is that $\varphi$ is high but conditional, and $\gamma$ is bounded by formalisation coverage rather than by proof-checking capability. Both caveats become central in §6.

3.2 Observed trajectory [E]

The trajectory is consistent with a system whose only binding constraint is generation quality.

At competition level, saturation arrived quickly. Multiple systems reached gold-medal performance at IMO 2025, with Seed-Prover and Gemini Deep Think each solving five of six problems. Earlier benchmarks such as miniF2F saturated, prompting the construction of harder ones — FrontierMath, and formalised Putnam problem sets covering analysis and abstract algebra beyond IMO scope. Benchmark saturation followed by benchmark replacement is precisely the signature of a generation-limited rather than verification-limited regime.

At research level, the record is more granular and more instructive. Erdős Problem #728 was resolved in January 2026 by a combination of GPT-5.2 Pro and Harmonic's Aristotle system, with the proof formalised in Lean; Tao publicly assessed it as more or less autonomous, in the spirit of the problem, and noted that no existing literature resolving it had been located. Three problems fell in a single week that month. Google's Gemini Deep Think solved Erdős Problem #1051 and contributed to a published paper. In April 2026, GPT-5.4 Pro produced a proof for Problem #1196 in roughly eighty minutes from a single prompt, which Tao described as a meaningful contribution to the anatomy of integers extending beyond the specific problem, and which became a co-authored May 2026 paper. DeepMind's Aletheia agent reports multiple publication-grade papers, including one produced without human intervention.

3.3 The caveats are the interesting part [E]

Three qualifications materially constrain what this record shows, and each is documented by the mathematicians closest to it rather than by external sceptics.

Selection effects on problem difficulty. Tao's own assessment is that greater AI involvement correlates with simpler underlying problems. Erdős problems are numerous, unevenly attended, and include a long tail that no one had prioritised. Solving a neglected problem is not the same as solving a frontier problem, and the systematic surveys note that successful full solutions concentrate on problems where the key insight, once found, yields a relatively short proof. Problems requiring sustained novel construction remain largely out of reach.

Literature-priority instability. The March 2026 addendum to Tao's original post on #728 records that the AI methods turned out to be very similar to those of a 2014 paper of Pomerance, who subsequently released a note showing that his earlier methods also resolve the problem. "No prior literature found" is a statement about search effort, not about novelty, and it is revisable.

The vacuity rate. Discussed above and in §6. It is the single most important number in this literature and the one least often quoted.

The honest summary: mathematics has demonstrated genuine AI contribution at the research frontier, at a rate that would be impossible without a near-ideal formal oracle, subject to caveats that the field is itself documenting with unusual rigour. That documentation quality is not incidental — it is downstream of the oracle. A field that can mechanically check its results can also mechanically audit its own hype.

4.1 Two oracles, not one [F]

Physics does not have a verification oracle. It has two, with almost complementary failure modes.

The simulation oracle ( $V_{\mathrm{s}\mathrm{i}\mathrm{m}}$): $\tau$ from seconds to weeks, $\kappa$ moderate to high, $\gamma$ high within the regime of validity of the governing equations, and $\varphi$ bounded by the fidelity of the model itself. A simulation cannot tell you that your Hamiltonian is wrong.

The experimental oracle ( $V_{\mathrm{e}\mathrm{x}\mathrm{p}}$): $\tau$ from hours to decades, $\kappa$ from thousands to billions of dollars, $\gamma$ low — most theoretical claims in contemporary physics are not experimentally adjudicable with existing apparatus — and $\varphi$ high, this being the whole point.

The structural consequence is a division of labour that the observed deployment pattern reflects exactly.

4.2 Where AI has succeeded, and why [E]

Consider the dominant success categories in AI-for-physics and note what they have in common.

Surrogate modelling. Neural networks trained to approximate expensive first-principles calculations — transport models, turbulence closures, neoclassical torque prediction, divertor plasma dynamics via neural PDE surrogates, heat-flux and magnetic-shadow calculation for fusion vessel design. In every case the oracle is the expensive simulation the surrogate replaces. $\gamma =1$ by construction: the ground truth is available for any input you care to spend on.

Control policy learning. Deep reinforcement learning for tokamak magnetic confinement; real-time kinetic profile reconstruction; disruption prediction with transfer learning across devices; adaptive control of cold-atom experiments. Here the oracle is the experiment itself, and it is unusually good — $\tau$ is a plasma discharge, $\varphi$ is high, and $\gamma$ is high for the specific question asked ("did the plasma stay confined?").

Pattern extraction from data. Identification of quantum phase transitions, anomaly detection in collider data, inference of entropy production from trajectory data.

The pattern is not subtle. AI has succeeded in physics precisely where a cheap, high-completeness oracle was already available or could be manufactured. Fusion is the clearest case: it is not an accident that the field with the most mature AI integration is one with hundreds of shots per campaign, dense diagnostics, and an unambiguous scalar success criterion.

4.3 Where AI has not succeeded [E/C]

The complementary observation is that AI has produced very little accepted fundamental physics — new laws, new theoretical structures, resolutions of open foundational questions. Efforts exist: benchmarks for scientific law discovery across physics domains, agents that derive physical laws from raw data, generative agents proposing equations with simulation feedback. Claims of AI-discovered new physics have appeared, including a recent case in dusty plasma where a custom neural network combined with laboratory data was argued to uncover a new interaction law, with the authors emphasising interpretability over black-box prediction.

We flag these as genuine but early [C]. The framework predicts why: for fundamental physics, ${\gamma }_{\mathrm{e}\mathrm{x}\mathrm{p}}$ is very low. Most theoretically interesting claims — about quantum gravity, about vacuum structure, about physics beyond the Standard Model — sit outside the reach of any oracle that can return a verdict this decade. A generator pointed at that space produces candidates that cannot be adjudicated, and unadjudicated candidates are not knowledge.

This makes a testable prediction, stated formally in §7: AI-driven fundamental physics progress will concentrate in the narrow band where new instrumentation has just opened experimental access, and will be near-absent elsewhere, irrespective of model capability.

4.4 Institutional response [E]

Institutions appear to be acting, whether or not they describe it this way, as though the oracle is the binding constraint. The U. S. Genesis Mission, launched by executive order in November 2025, is explicitly structured to couple AI models to experimental facilities, supercomputers, and data archives across the national laboratory system. PPPL's STELLAR-AI platform connects computing resources directly to experimental devices including NSTX-U, so that data can be analysed as experiments occur.

Read through the framework, this is oracle engineering: reducing $\tau$ by closing the loop between generation and experimental adjudication. It is the correct intervention. Whether it is sufficient is open.

5.1 Oracle parameters

Biology's oracle is the weakest of the three on nearly every axis. $\tau$ ranges from days for a cell assay to years for a clinical endpoint. $\kappa$ is high and, crucially, does not fall with scale in the way computation does. $\gamma$ is low: most biological claims worth making concern in-vivo or clinical behaviour and cannot be adjudicated by any available assay. $\varphi$ is the axis on which biology fails most distinctively — even a completed experiment returns a noisy verdict, and reproducibility problems are endemic in a way they simply are not in proof checking.

5.2 The AlphaFold exception, correctly diagnosed [E]

Protein structure prediction is the great success of AI in biology, and the framework explains it as an oracle story rather than a modelling story.

Structure prediction had, uniquely within biology, a near-ideal oracle: the Protein Data Bank. Roughly 200,000 experimentally determined structures, standardised, curated, with an unambiguous scalar accuracy metric (GDT), and a biennial blind evaluation in CASP that no participant could game. The oracle was pre-built, at enormous cost, by decades of crystallography and cryo-EM.

The trajectory followed: AF1 at CASP13 in 2018 using convolutional networks for inter-residue distances, AF2 at CASP14 in 2020 with a transformer architecture and median GDT above 90, AF3 in 2024 extending to protein–ligand, protein–nucleic acid, and protein–protein complexes. Over 200 million predicted structures were released. The 2024 Nobel Prize in Chemistry recognised Hassabis and Jumper for AlphaFold and Baker for computational design.

Two observations sharpen the diagnosis.

First, the impact pattern matches oracle theory rather than capability theory. A Berkeley Haas study by Hill and Stein finds that AlphaFold2 broadened the range of proteins researchers were willing to study — Stein's characterisation is that it functions as a floodlight directing attention beyond the small subset the community had focused on — while translation into medicines remains constrained by downstream work and regulatory bottlenecks. In our terms: AlphaFold improved $R_{\mathrm{g}\mathrm{e}\mathrm{n}}$ for structural hypotheses. It did not improve $R_{\mathrm{v}\mathrm{e}\mathrm{r}}$ for therapeutic ones. The bottleneck moved but did not lift.

Second, and importantly for the framework's honesty, AlphaFold's failure modes cluster exactly where the oracle is thin. Multiple 2024–2026 analyses report that predictions of alternative and fold-switched conformations are substantially driven by structure memorisation, with memorisation bias documented for solute-carrier membrane proteins and alternative-state modelling assessed as a distinct challenge in CASP16. Conformational ensembles are underrepresented in the PDB. The model is excellent where the oracle was dense and unreliable where it was sparse. This is a strong confirmation of the framework, and one we did not construct the framework to accommodate.

5.3 Agentic biology and the wall [E]

The agentic wave has arrived. DeepMind's Co-Scientist, built on Gemini and orchestrating specialised agents that generate, debate, rank, and evolve hypotheses, published in Nature in May 2026 alongside FutureHouse's Robin and a third DeepMind tool for scientific software generation. Robin reviewed the dry AMD literature, hypothesised FDA-approved candidates, designed preclinical assays, and identified ripasudil — a glaucoma drug — with lab tests confirming a real effect; Robin also analysed the resulting RNA-seq data and proposed ABCA1 as a possible new target. The Co-Scientist was applied to an open problem in bacterial gene transfer and produced novel testable hypotheses that aligned with independently obtained empirical findings; the authors describe the design as scientist-in-the-loop, prioritising cognitive collaboration over full automation. A DeepMind–Yale single-cell model generated a since-validated hypothesis about silmitasertib rendering "cold" tumours immunologically visible.

These are real results. And the reported constraint is invariant across all of them: Robin could propose experiments very rapidly, but obtaining reagents and waiting for cells to grow took weeks.

That sentence is the paper's thesis in miniature. $R_{\mathrm{g}\mathrm{e}\mathrm{n}}$ has increased by orders of magnitude. $R_{\mathrm{v}\mathrm{e}\mathrm{r}}$ has not moved. $R=\min (\cdot ,\cdot )$ is unchanged.

5.4 The virtual-cell wager [E/C]

The most direct attempt to attack the oracle rather than the generator is the virtual cell programme — the construction of computational world models that predict how genetic and chemical perturbations produce transcriptional responses. Recent work has begun to automate the construction of such models: VCHarness, an autonomous system combining a coding agent with multimodal biological foundation models, explores large spaces of architectures and training pipelines with minimal human intervention, and is reported to uncover non-obvious architectural patterns associated with improved performance.

Read through the framework, a virtual cell is an attempt to build a cheap $V_{\mathrm{s}\mathrm{i}\mathrm{m}}$ for biology — to give the field the second oracle that physics already has. This is the correct strategic target. It also inherits physics' problem: a simulation oracle's $\varphi$ is bounded by the fidelity of the simulation, and biology's models are far from the position of, say, computational fluid dynamics. There is a circularity risk here that deserves explicit naming: a virtual cell trained on perturbation data, used to adjudicate hypotheses about perturbation responses, can only certify claims that are interpolations of its training distribution. The value of an oracle lies precisely in its capacity to return verdicts the generator could not have predicted. We flag as an open problem whether learned simulators can supply genuinely independent verdicts, or whether they merely relocate the generator's own inductive biases into the verification step [C].

6.1 The ordering Latency $\tau$ Cost $\kappa$ Completeness $\gamma$ Fidelity $\varphi$ Observed AI autonomy Mathematics ms–min ~0 Medium–high ~1 (conditional) Autonomous solutions to open problems Physics (sim) s–weeks Medium High in-regime Model-bounded Autonomous surrogates, control policies Physics (exp) h–decades High–extreme Low High Assisted; near-zero autonomy in fundamentals Biology (assay) days–years High Low Medium Hypothesis generation only; human-validated Biology (PDB) pre-built Sunk High for native folds High Near-solved structure prediction

The last column was not fitted to the first four. The ordering falls out.

The internal split within biology is the framework's strongest evidence. The same field, the same models, the same year — but structure prediction, with a pre-built oracle, is approximately solved, while therapeutic hypothesis generation, without one, is stuck at scientist-in-the-loop. If domain difficulty or model capability were the operative variable, this split would not exist.

6.2 The vacuity mechanism, generalised [C]

The Erdős vacuity finding is not a quirk of mathematics. It is the general signature of an oracle with high $\varphi$ on formal validity and $\gamma =0$ on significance.

Any optimiser directed at a proxy will exploit the gap between proxy and target. Where the oracle measures formal correctness only, an optimiser will find the region of claim-space that is maximally easy to make formally correct — which is, definitionally, the trivial region. The result is a system that passes verification at high rates while contributing nothing, and — worse — a body of literature that looks like progress under automated audit.

The same mechanism has domain-specific forms:

• —Physics. A surrogate optimised against simulation output learns the simulation's artefacts alongside its physics. A control policy optimised for a scalar reward finds the degenerate strategy that maximises the reward without achieving the intent.
• —Biology. A model optimised against a structural database learns to memorise structures rather than to fold, which is exactly what the conformational-state analyses report.

The general prescription follows: significance cannot be delegated to the same oracle that checks correctness. Where a field lacks a significance oracle — and all three lack one — human judgment remains structurally necessary, not as a transitional accommodation but as a permanent component of the verification stack. This is a stronger and less comfortable conclusion than the usual "human-in-the-loop for now" framing.

6.3 The strategic inversion

If the framework holds, the field's dominant investment thesis is misallocated at the margin. Resources flow overwhelmingly to generation — larger models, better reasoning, more agentic scaffolding. But in two of three domains examined, generation is not the binding constraint.

The high-leverage interventions are:

• —Formalisation coverage in mathematics.
• —$\gamma$, not $\varphi$, is mathematics' binding constraint; the bottleneck is getting statements into formal form. The NSF's Institute for Computer-Aided Reasoning in Mathematics, launched in late 2025, targets exactly this.
• —Closed-loop experimental facilities in physics. Reducing ${\tau }_{\mathrm{e}\mathrm{x}\mathrm{p}}$ by coupling generation directly to apparatus — the Genesis Mission and STELLAR-AI thesis.
• —Automated wet-lab infrastructure in biology. Robotic cloud labs attack $\tau$ and $\kappa$ directly. This is unglamorous, capital-intensive, and probably the single highest-return investment in AI-for-biology.
• —Significance oracles everywhere. The hardest and least-attempted. What would it mean to mechanically check that a result matters? We do not know, and we suspect the honest answer is that it cannot be fully mechanised. But partial progress — automated novelty checking against literature, automated triviality detection, automated statement-intent verification — is tractable and underexplored.

The framework is worth little unless it can be wrong. Six predictions, with explicit failure conditions.

P1 — Oracle-first ordering. Across any set of scientific subfields, the degree of demonstrated AI autonomy will correlate more strongly with oracle quality (as operationalised by $\tau$, $\kappa$, $\gamma$, $\varphi$) than with any measure of intrinsic problem difficulty or with model capability at time of deployment. Falsified by: a subfield with a weak oracle achieving autonomous, community-accepted discovery at rates comparable to formal mathematics.

P2 — The biology autonomy gap persists. Absent a step-change in wet-lab throughput, the ratio of AI-generated biological hypotheses to experimentally validated AI-generated biological findings will not improve materially over the next 36 months, regardless of model improvements. Falsified by: validated-finding rate scaling with model capability while assay throughput remains flat.

P3 — Instrumentation gates fundamental physics. AI contributions to accepted fundamental physics will cluster within roughly five years of new instrumentation opening experimental access to a regime, and will be near-absent in regimes with no near-term experimental access. Falsified by: an AI-originated theoretical result in an experimentally inaccessible regime achieving community acceptance on non-empirical grounds.

P4 — Vacuity scales with autonomy. As autonomous generation increases in any domain, the fraction of formally-valid-but-insignificant output will rise, not fall, unless a significance oracle is deliberately constructed. Falsified by: rising autonomy accompanied by falling vacuity rates with no change in significance-checking procedures.

P5 — Oracle-density predicts model reliability. Within a single trained model, prediction reliability will track training-oracle density across subregions of the domain. The conformational-state findings in AlphaFold are one instance; the prediction is that this generalises. Falsified by: a model showing uniform reliability across regions of markedly differing oracle density.

P6 — Oracle investment outperforms model investment at the margin. In domains where $R_{\mathrm{v}\mathrm{e}\mathrm{r}}<R_{\mathrm{g}\mathrm{e}\mathrm{n}}$, a fixed budget spent on verification infrastructure will yield more validated discoveries than the same budget spent on generative capability. Falsified by: a controlled comparison — admittedly difficult to construct — showing the reverse.

P6 is the practically important one and the hardest to test cleanly. We flag this asymmetry rather than paper over it.

The framework is descriptive, and post-hoc. It was constructed after observing the pattern it explains. Its predictive content rests entirely on §7, which is untested. A framework that explains everything already observed and predicts nothing new is a story, not a theory.

Oracle parameters are not currently measurable. We have written $\tau$, $\kappa$, $\gamma$, $\varphi$ as though they were quantities. They are, at present, qualitative rankings. A serious version of this argument would operationalise them — median adjudication latency, dollars per adjudication, fraction of arXiv claims in a field mechanically checkable. We have not done this, and the framework's quantitative claims should be read as ordinal.

Selection bias in the evidence base. AI successes are reported; failures are not. The mathematics record is unusually well-documented precisely because Tao and collaborators chose to document it, including the embarrassing parts. No comparable audit exists for physics or biology, so the comparison across domains is between a well-audited field and two poorly-audited ones. This cuts against our confidence in the ordering, and we do not know by how much.

Source quality is uneven. Claims here rest on a mix of peer-reviewed papers, preprints, institutional communications, and journalism. Several load-bearing items — particularly around autonomous prover systems — are supported primarily by non-peer-reviewed reporting and are tagged accordingly in Appendix A. We have excluded several widely-circulated claims about AI-resolved major conjectures that we could not trace to a primary source.

The framework may be a tautology in disguise. "Progress is limited by what you can verify" risks being true by definition of "progress." The non-trivial content, if any, is the orthogonality to difficulty claim of §2.3 and the within-biology split of §6.1. If those two survive scrutiny, the framework has content. If they do not, it does not.

The prevailing account of AI in science is a capability account: models get better, science gets faster. The evidence of 2025–2026 does not fit it. The same models, in the same year, produced formally verified resolutions of open mathematical problems, fast surrogates for plasma physics calculations, and hypotheses that biologists then spent weeks testing by hand. The difference was not in the models.

The difference was in what each field can cheaply check.

Mathematics built a verification oracle over four decades of work in formal methods that most of the field regarded as a niche concern of logicians. That investment now looks like the most consequential infrastructure decision in the discipline's recent history. Structural biology built one too, at enormous expense, and called it the Protein Data Bank; AlphaFold is what happened when a sufficient generator met a sufficient oracle. Where no such oracle was built — fundamental physics, therapeutic biology — the arrival of powerful generators has produced abundant candidate knowledge and very little confirmed knowledge.

The framing we have argued for throughout is that this is not a prohibition but a specification. Nothing forbids autonomous discovery in biology. What is required is stated precisely: an adjudication procedure with latency measured in hours rather than weeks, marginal cost low enough to permit search rather than selection, coverage extending to the claims that actually matter, and fidelity sufficient that its verdicts can be trusted without replication. That specification is demanding. It is not impossible. It is, notably, a different research programme from the one currently receiving most of the funding.

One conclusion resists this optimism, and we state it plainly rather than soften it. The vacuity finding suggests that the significance layer of verification may not be mechanisable at all. An oracle can tell you a proof is correct. Nothing we know how to build can tell you the theorem was worth proving. If that limit is real rather than merely current, then the endpoint of this trajectory is not autonomous science but a permanent division of labour in which machines generate and verify, and humans decide what was worth generating.

The cartoon closes. The real problem stays open.

Every load-bearing claim, classified by layer and epistemic status. Layer: E = empirical, F = framework/definitional, C = conjecture. Status: Documented / Reported / Proposed / Open.

Claim Layer Status Support Falsification condition

1. 1.AI systems reached IMO gold-medal performance in 2025 (5/6 problems, multiple systems) E Documented Multiple independent surveys and primary announcements Retraction of scoring; independent audit showing lower performance
2. 2.Erdős #728 was resolved with AI as primary contributor, formalised in Lean, no prior literature located at the time E Documented Tao public assessment; arXiv writeup of the Aristotle proof Discovery of prior resolving literature — partially realised, see #3
3. 3.The #728 methods closely resemble a 2014 Pomerance paper, which also yields a solution E Documented Tao's March 2026 addendum Retraction of Pomerance note
4. 4.A substantial fraction of Aletheia's "correct" Erdős solutions were technically valid but mathematically vacuous E Documented Feng et al. semi-autonomous evaluation, 700 problems Re-grading under a different rubric yielding materially different rates
5. 5.Tao assesses greater AI involvement as correlating with simpler underlying problems E Documented Public statements; wiki caveats Frontier problems falling to AI at comparable rates
6. 6.AlphaFold2 achieved near-experimental accuracy on single-chain folds (median GDT > 90 at CASP14) E Documented CASP14 results; Jumper et al. 2021 — (settled)
7. 7.AlphaFold predictions of alternative/fold-switched conformations are substantially driven by memorisation E Documented Multiple 2024–2026 analyses; CASP16 alternative-state assessment Demonstration that fold-switch prediction generalises out-of-distribution
8. 8.Robin (FutureHouse) proposed ripasudil for dry AMD with subsequent lab confirmation of effect E Reported Nature 2026 publication; contemporaneous reporting Failure to replicate the ripasudil effect
9. 9.Wet-lab timelines, not hypothesis generation, are the reported rate-limiting step in agentic biology E Reported Direct statements in reporting on Robin Documented case of validated-discovery rate rising with model quality at flat assay throughput
10. 10.AI is deployed in fusion primarily as surrogate, controller, and predictor rather than as theory generator E Documented PPPL programme descriptions; extensive ML-for-tokamak literature An accepted, AI-originated fundamental result in plasma theory
11. 11.Verification oracles can be characterised by latency, cost, completeness, fidelity F Proposed — (definitional) Not falsifiable; assessed on utility
12. 12.Useful output rate is bounded by min(generation rate, verification rate) F/C Proposed Search-theoretic argument, §2.2 Sustained discovery at rates exceeding adjudication capacity
13. 13.Oracle quality is orthogonal to intrinsic problem difficulty C Proposed §2.3 argument; within-biology split, §6.1 Demonstration that a difficulty metric predicts AI autonomy better than oracle quality
14. 14.Autonomy is bounded above by oracle quality largely independent of generative capability C Open — central claim §§3–6, pattern consistency P1, P2, P6 of §7
15. 15.Low significance-completeness necessarily produces formally-valid-but-vacuous output under optimisation pressure C Proposed Erdős vacuity data; proxy-optimisation argument P4 of §7
16. 16.Learned simulators (virtual cells) may not supply verdicts independent of the generator's inductive biases C Open problem §5.4 circularity argument Demonstration of a learned simulator producing verdicts that reliably contradict and correct its generator
17. 17.Significance verification may not be mechanisable even in principle C Open problem §9 Construction of a working significance oracle
18. 18.Marginal returns favour oracle investment over model investment where verification is the bottleneck C Proposed §6.3 P6 of §7

Ledger note. Claims 14, 16, and 17 carry the argument. All three are conjectures. The paper's contribution, if it has one, is the specification of what would settle them — not their settlement.