Beyond the Theorem Race: Is AI’s Jagged Scientific Frontier Flattening?

An evidence-based assessment of AI research systems, formal mathematical infrastructure, executable software verification, scientific discovery, and the empirical meaning of a flattening scientific capability frontier.

Introduction: from mathematical breakthroughs to a possible transformation of scientific research

The question raised by the latest mathematical AI results is no longer whether neural networks can solve difficult mathematical exercises. Systems developed by competing organizations now contribute to research-level investigations, construct extensive machine-checked formalizations, and coordinate long sequences of exploratory and verification tasks. Meanwhile, related methods are appearing in software assurance, theoretical physics, and laboratory-connected science. It is tempting to interpret these developments as evidence that an initially uneven landscape of AI capabilities is becoming uniformly tractable. That interpretation, however, goes beyond what isolated breakthroughs can establish.

The original jagged technological frontier described an uneven pattern of success and failure among tasks that might appear similar to human observers. Dell’Acqua and colleagues found that GPT-4 assistance could substantially improve consultants’ performance on some assignments and impair it on others. Their result concerned a particular experimental task distribution, not a geometrical boundary or a universal claim about scientific disciplines.¹ Generalizing this concept to science requires specifying what counts as success, whose resources are included, which problems are comparable, and what evidence justifies acceptance of an output.

There are at least three hypotheses that should not be confused. Frontier expansion means that systems complete tasks previously beyond their reliable capabilities. Capability convergence means that performance disparities among scientifically comparable task classes decrease. Scientific infrastructure formation means that models, verification engines, structured knowledge, software, and instruments become organized into a system whose outputs can be preserved and reused. The first is strongly suggested by the 2026 record. The second is plausible but unmeasured in a sufficiently comparable cross-disciplinary study. The third may be the most consequential transformation, since scientific progress depends on the durability and interpretability of results, not merely their generation.

These distinctions arise from the logic of research itself. A mathematically correct derivation is correct relative to the assumptions and formal statement it establishes. A verified executable is correct only with respect to specified behavioral properties and a sufficiently faithful execution model. A theoretical prediction may follow deductively from a physical model while the applicability of that model remains empirically unsettled. A reported laboratory discovery requires measurements and controls; an archival reconstruction requires evidence of original authorship as well as mathematical validity. No common achievement label, including solved, makes these forms of assurance equivalent.

A second source of ambiguity is the unit of intelligence being evaluated. A foundation model operating on a single prompt is not identical to a research harness coordinating many agents, importing external libraries, running computational experiments, and rejecting invalid candidates. If the aim is to assess research systems available to scientists, it is appropriate to evaluate the complete arrangement. If the aim is to identify progress in a model’s intrinsic reasoning, changes in tools, feedback, human guidance, and inference expenditure must be controlled.

The analysis therefore proceeds from the concrete achievements and architectures to a formal account of capability, then tests that account against software verification and empirical science. It also considers the recovery of historical mathematical knowledge, where formal correctness and authorship attribution become distinct obligations. Finally, it examines the economics of research generated faster than it can be independently evaluated and proposes a longitudinal measurement program. The conclusion is deliberately narrower than either an imminent general-scientist narrative or a dismissal of the achievements as sophisticated pattern matching: increasingly powerful computational research systems are emerging, but the shape and reliability of their scientific frontier remain empirical questions.

From OpenAI’s breakthroughs to a competitive ecosystem of mathematical intelligence

The transformation of mathematical AI is occurring through competition among different technical and organizational approaches rather than the linear extension of one model. DeepMind’s AlphaGeometry demonstrated a combination of learned construction and symbolic deduction in geometry, while AlphaProof and later Gemini Deep Think systems extended the scope of AI reasoning on Olympiad and professional problems. In July 2025, an advanced Gemini Deep Think configuration reached gold-medal standard at the International Mathematical Olympiad; this was a consequential benchmark achievement, not a demonstration of autonomous research on arbitrary open conjectures.²³

On October 6, 2026, OpenAI released a broad collection of AI-generated mathematical results through a public repository, with some Lean formalizations, revision procedures, information about attempted problems, and estimates of inference expenditure. The company reported that an average result consumed computation equivalent to roughly three hours of ChatGPT Pro thinking. This was not an independent estimate of the total cost of producing accepted mathematical knowledge, because failed attempts, expert examination, semantic review, and later corrections also matter. The large release created a new problem for the mathematical community: results could be generated and published more rapidly than human researchers could assimilate, explain, and evaluate them.⁴

OpenAI’s research announcements during 2026 made a different kind of claim: internal systems had contributed to previously unresolved mathematical questions and generated research artifacts, some accompanied by Lean formalizations. The October 26 announcement included a proposed refutation of the Exponential Time Hypothesis, a local-smoothing result with consequences for other harmonic-analysis conjectures, and more restricted materials concerning constructive quantum field theory. For ETH and local smoothing, the company released mathematical writeups and proof artifacts; for some field-theoretic claims, access was initially organized through designated expert groups. These differences in availability matter when assessing independent reproducibility and scientific acceptance.⁵

Anthropic approached related questions through Claude-based mathematical research, formalization, and specialized investigations. An August report described a model-generated improvement in a lower bound concerning zeros of the Riemann zeta function, without claiming a proof of the Riemann hypothesis. Its November Claude Fable and Mythos 5.2 release reported rapid formalization of Fermat’s Last Theorem using a large coordinated agent population, alongside new theoretical-physics calculations. These claims vary in the extent of public proof material and independent review; the mathematics should be evaluated at the level of individual theorem statements, not inferred from the capabilities of a model family.⁶⁷

Google’s research direction emphasizes both stronger models and reusable agentic orchestration. Aletheia, developed with Gemini Deep Think, uses generation, verification, and revision to improve research-level mathematical performance; importantly, its design allows a verifier to reject a candidate or acknowledge failure rather than treating every candidate as progress. Google’s Antigravity Teamwork subsequently generalized long-horizon coordination beyond pure mathematics, with separate patterns for proof construction, coding, and document review.⁸⁹

Axiom Math represents a complementary strategy: it treats formalized mathematics as a reusable computational substrate. Its October 26 announcement of a massive Lean development for the classification of finite simple groups was followed by a formalization of the Stacks Project, the Weil conjectures, and Faltings’ theorem. The organizational objective differs from solving a leaderboard problem. It is to make the definitions, theorems, and dependencies of extensive mathematical theories available for later machine-checked work.¹⁰¹¹

Competition can accelerate several variables independently: model reasoning, test-time search, automated formalization, orchestration quality, and access to large verified libraries. An impressive result may come from one exceptional model attempt, from many parallel attempts selected by a reliable verifier, or from a mature library that makes a new proof almost routine. Without separating these causes, comparative statements about which laboratory possesses superior scientific intelligence become misleading.

The diversity is nevertheless significant. Different research groups are building mechanisms that can be recombined, from deductive checking and semantic retrieval to agent critique and experimental feedback. That convergence of infrastructure is real even before there is evidence of convergence in task-level reliability.

What the laboratories have actually achieved

The range of achievements compared in Table 1 begins with a simple point: the label mathematical breakthrough covers events with different epistemic status. Winning a competition, finding a new theorem, rediscovering an old result, formalizing an established proof, producing a partial result, and releasing an as-yet-unexamined mathematical claim should not be counted as equivalent achievements. Their practical significance depends on the exact proposition, the proof or experiment offered, and the extent of independent scrutiny.

Achievement class	What the result establishes or suggests	Main residual question
Competition performance	Success on a fixed, high-difficulty test distribution	Generalization to genuine open research
New mathematical claim with public proof	A research-level candidate available for mathematical scrutiny	Validity, novelty, and interpretability
Kernel-checked formalization	A specified formal proposition follows from its declared foundations	Fidelity to the intended informal theorem
Formalization of an existing theory	A reusable dependency structure can be checked computationally	Library quality, scope, and maintenance
Theoretical scientific calculation	A result follows within a specified mathematical or computational model	Physical relevance and independent confirmation
Laboratory-assisted result	Measurable outcomes improve under tested conditions	Replication and generalization to other settings

Table 1: Different evidentiary meanings of recent AI-assisted scientific achievements.

The distinction is particularly useful for the high-profile October and September 2026 claims. OpenAI announced a deterministic subexponential-time algorithm that, if valid with its claimed asymptotics and formal correspondence, refutes the Exponential Time Hypothesis. The public mathematical material and a reported Lean proof make the claim open to further review, but its implications for the complexity-theory literature require independent mathematical adjudication. OpenAI also claimed a smooth-forcing finite-time singularity for three-dimensional Navier–Stokes, with an analytical writeup and Lean artifact. The official Clay formulations C and D admit particular smooth forces; the presence of forcing is therefore not by itself a reason to dismiss the claim. Equally, the claim is not automatically a result about unforced flows, and prize recognition is a distinct process.¹²¹³

Anthropic’s Riemann-zeta work illustrates the importance of describing a partial result accurately. Improving a bound on the proportion of zeros satisfying the Riemann hypothesis would be mathematically valuable if validated, but it would not prove that all nontrivial zeros lie on the critical line. Likewise, its November holographic physics preprints concern precise mathematical models and asymptotic statements, not laboratory observations of black holes.¹⁴¹⁵

For mathematical formalization, the contrast between theorem checking and source meaning becomes decisive. A Lean kernel establishes that a proof term has the asserted type under the imported definitions and axioms. It does not determine whether the theorem was intended, whether a reference text was faithfully transcribed, or whether a result is new. These questions require separate semantic, historical, and scientific review.

Research-level evaluation is also affected by the way a candidate was selected. A result obtained after tens of thousands of attempts under heavy compute expenditure provides different information about individual-attempt reliability from a result obtained reliably with a fixed modest budget. Both can have value; their evidence about generality differs. Thus the immediate task is not to reduce every announcement to one ranking, but to characterize the mechanisms and validation standards that produced the work.

Axiom Math: from formal proofs to a cumulative mathematics infrastructure

The Axiom program reveals a transformation more fundamental than an increase in the number of formalized theorems. Classical proof formalization often constructed a specialized development whose definitions and lemmas were chosen to reach one target. A reusable mathematical infrastructure reverses that priority: foundational definitions and stable interfaces are built with the intention that many subsequent investigations will reuse them. The criterion of success becomes not only whether a final theorem typechecks, but whether the entire formal dependency structure is correct, interpretable, maintainable, and portable to new research problems.

In October 2026 Axiom reported that its system, under the direction of mathematicians and engineers, produced approximately 43.1 million lines of Lean over 24 days to formalize the classification of finite simple groups. The theorem identifies all finite simple groups, including cyclic groups of prime order, alternating groups of degree at least five, the families of Lie type, and the 26 sporadic groups. Its human proof corpus was distributed across hundreds of articles and thousands of pages, so the formalization required a vast web of prerequisite definitions, lemmas, and case analyses.¹⁶

Axiom’s project map organized 108 milestones and numerous subordinate obligations. A formal proof of a conditional lemma can advance a dependency graph while leaving the condition unproved; consequently, a dashboard of completed subtasks is not proof that the final theorem has been established. Completion requires a checked chain from the foundational environment to the final classification statement, with no unresolved placeholders or unauthorized assumptions.

The project reported 34 noteworthy deviations from the mathematical literature, including a problem in an existing treatment of the Unbalanced Group Theorem. The team consulted established group theorists and formalized alternative reasoning that repaired the required argument. This is evidence for an additional value of formalization: an informal proof accepted through expert mathematical practice can contain omissions or inaccurate intermediate statements that become explicit when each dependency must be checked. At the same time, an agent’s inability to formalize a step is not evidence that the original step is false; the defect may instead be in the agent’s interpretation.

The logical guarantee can be expressed as a typing judgment:

\Gamma\vdash p:P, \tag{1}

where () is the formal environment, (P) a proposition, and (p) a proof term accepted by the checker. If the theorem imports declarations through a dependency graph (G=(V,E)), its effective trusted mathematical context includes the transitive dependency closure (D_G(P)), not merely the lines of code displayed in the final theorem. Meaningful review therefore requires provenance for imported results and the foundations on which they rely.

Axiom’s subsequent Stacks Project release extends this principle. The company reported approximately 16 million lines of Lean corresponding to the roughly 7,500-page Stacks Project, with declarations linked to the reference text through stable tags. Its documentation distinguishes a human-reviewed core from AI-produced frontier material that has not received the same semantic review. Both may contain machine-checked proofs, but they do not have identical claims to editorial and mathematical fidelity.¹⁷

The formalization of the Weil conjectures and Faltings’ theorem illustrates the potential cumulative benefit. Both depend on substantial algebraic-geometric infrastructure that can be reused rather than reconstructed. Axiom reports that its Bombieri–Vojta development of Faltings’ theorem contains approximately 110,000 lines of proof-specific Lean code built on millions of lines of shared formal foundations. The number of lines is not itself a measure of mathematical insight, but reuse of compatible and verified prerequisites can change the cost structure of subsequent research.¹⁸¹⁹

The key unresolved question is semantic completeness. Let (S) be a set of statements in an informal source corpus and (V) the declarations of its formalization. A documented relation

R\subseteq S\times V \tag{2}

can record which declaration is intended to represent which source statement, but a repository full of checked declarations does not mechanically prove that every pair in (R) is faithful. Nor does it show that the source corpus is completely covered. The stronger claim must be supported through explicit source mappings, semantic review, and audits of high-dependency assumptions.

The resulting architecture can be represented as a graph of mathematical and evidentiary dependencies, not as a simple sequence of automated proofs. As Figure 1 emphasizes, a formal proof and the corresponding source interpretation are different artifacts that must remain connected.

%%{init: {"theme": "neo", "look": "handDrawn", "layout": "elk"}}%%
flowchart TD
    A[(Mathematical source corpus)] -->|supplies statements| B(Interpret and formalize)
    B -->|publishes declarations| C[(Versioned Lean library)]
    C -->|supplies dependencies| D(Proof construction)
    D -->|submits terms| E{Kernel accepts?}
    E -->|yes| F[(Checked theorem)]
    E -->|no| D
    G[Human mathematical review] -.->|validates correspondence| B
    G -.->|approves status| F
    F -->|reusable formal result| C

Figure 1: Reusable mathematical infrastructure separates machine-checked proof dependencies from the source-to-formal interpretation that gives a library its scientific meaning.

A mathematical library becomes scientific capital when later researchers can rely on its definitions, theorem statements, and provenance. Kernel correctness is necessary for that goal but insufficient without source fidelity and maintained interfaces. The important transition is from a proof that closes one obligation to an infrastructure capable of supporting a succession of new obligations.

The research harness becomes part of the scientific method

If formal libraries provide a substrate, the research harness provides the operational environment in which the substrate can be exploited. It determines how candidate strategies are proposed, how evidence is retained, when a problem is subdivided, how tools are invoked, which objections are preserved, and when a result is eligible for independent review. For long-horizon tasks, these choices can be as consequential as the performance of the underlying reasoning model.

Stellar Colosseum, described by Lin and colleagues in September 2026, explores competing research strategies, subjects them to falsification, applies a readiness gate before large-scale decomposition, and represents the resulting proof plan as a graph of dependent subproblems. Parallel investigators can work on independent obligations, while later stages must wait for relevant prerequisites. Critiques and failed approaches remain available as research evidence rather than being discarded as unproductive dialogue.²⁰

The dependency structure places a lower bound on elapsed completion time. Let (H=(W,F)) be a directed acyclic graph of research tasks, let (t_v) denote task (v)’s execution duration, and let (P(H)) denote its directed paths. Then, absent overlap within a task,

T_{\mathrm{wall}}\geq\max_{\pi\in\mathcal P(H)}\sum_{v\in\pi}t_v. \tag{3}

Increasing the number of agents cannot break this critical-path constraint without changing the task decomposition or accelerating the stages on the longest path. More parallelism can also increase total inference cost and the burden of reconciling inconsistent outputs. An agent count therefore measures neither scientific productivity nor proof reliability by itself.

Colosseum’s reported results illustrate the difference between a model and its surrounding system: its harness changes performance on research-level theoretical computer science problems by allocating more computation to alternative strategies, review, and revision. Google’s Antigravity Teamwork adapts similar ideas to mathematical proofs, scientific software, hardware simulation, and document criticism, while a November research report describes specialized patterns that combine Gemini models with external checkers and targeted computational feedback.²¹

These architectures are not merely prompt templates. A persistent research system needs durable task definitions, explicit interfaces between subtasks, a record of failed assumptions, a versioned artifact store, and the ability to reconstruct which evidence supports a conclusion. Without that state, an apparently long-running investigation may actually consist of disconnected model outputs that are difficult to audit or reproduce.

The operational distinction depicted in Figure 2 applies equally to independent review. A second agent that receives the first agent’s assumptions may repeat the same mistake. A critic with access to a formal checker can reject invalid inferences, but only relative to the specification provided. A simulation can refute a candidate under modeled conditions; it cannot establish the model’s complete physical validity. In every case, the verifier’s authority must be bounded by the type of evidence it can produce.

The architecture in Figure 2 illustrates how strategy selection, execution, independent feedback, and durable provenance can be separated.

%%{init: {"theme": "neo", "look": "handDrawn", "layout": "elk"}}%%
flowchart TB
    A[Research objective] --> B(Competing strategies)
    B --> C{Ready to decompose?}
    C -->|no| B
    C -->|yes| D[(Dependency-aware task plan)]
    D --> E(Parallel research tasks)
    E --> F{Independent evaluation}
    F -->|rejected or incomplete| G[(Failure and critique record)]
    G -->|revises strategy| B
    F -->|accepted within scope| H[(Validated artifact and provenance)]
    H -->|reusable dependencies| D
    I[Human research authority] -.->|sets objectives and acceptance criteria| A
    I -.->|approves scientific interpretation| H

Figure 2: An auditable research harness separates exploratory computation, evaluation, and durable evidence; unsuccessful attempts remain available to subsequent investigations.

Google’s opt-in manuscript review experiment before STOC 2027 underscores a related institutional role: a research harness can support not only discovery but the detection of mathematical errors before publication. Yet survey satisfaction and the fraction of submitted manuscripts receiving feedback cannot be converted into proof that the system is an independently reliable peer reviewer. Selection effects, common-mode errors, and the absence of final external adjudication remain relevant.

The most consequential distinction is between an AI answer and an AI research process capable of preserving structured evidence. Harness design can improve outcomes without increasing the correctness of a model’s first attempt. Whether that improvement generalizes across scientific domains depends on what forms of verification each domain makes possible.

Formalizing the jagged scientific frontier

The expression jagged scientific frontier is an explanatory metaphor until its measurement domain, success criterion, and comparison conditions are defined. Scientific problems have no intrinsic common coordinate system. A theorem whose proof has resisted mathematicians for decades, a complex program-verification task, and a laboratory experiment whose preparation takes three weeks cannot be placed on one objectively ordered difficulty axis without assumptions about the reference population and the kind of work being measured.

Let (X=_dX_d) denote a prespecified population of tasks divided into domains or task families (d). Each task (x) has descriptors (z(x)), including difficulty, epistemic regime, required tools, novelty, ambiguity, and degree of available verification. Let (c) denote the complete evaluated research configuration, (t) the evaluation date, (b) a resource budget, and (v) an explicit validation protocol. Define

p_{c,t}(x;b,v)=\Pr\bigl\{\mathcal V_v[c(x;b)]=1\bigr\}, \tag{4}

where (V_v) is the procedure used to judge successful completion. This probability is conditional on the chosen system, repeated-run protocol, and verifier. If a verifier has false-positive or false-negative errors, the measured probability is not identical to the probability that the underlying scientific claim is true. The reliability of the evaluation itself must therefore be characterized.

At a target reliability (), the capability frontier can be represented as a level set,

F_{c,t}(\tau,b,v)=\{x\in\mathcal X:p_{c,t}(x;b,v)\geq\tau\}. \tag{5}

This is not automatically a geometric boundary: scientific tasks have neither a natural metric nor a universally agreed ordering. Given a fixed task-distribution measure (), the coverage of reliable capability is ((F_{c,t})). Frontier expansion between periods is described by newly covered tasks (F_{c,t_1}F_{c,t_0}), while regression is described by the reverse difference. Improvements in average benchmark score do not establish that the frontier expands monotonically, because changes in systems and tools can create regressions in particular task families.

A measure of flattening must capture heterogeneity rather than simply coverage. Suppose comparable domain success probabilities have been calibrated at fixed difficulty (z), with domain weights (w_d) satisfying (_d w_d=1). Define the mean capability

\bar p_{c,t}(z;b)=\sum_{d=1}^{D}w_d p_{c,t}(d,z;b), \tag{6}

and a difficulty-conditioned dispersion statistic

J_{c,t}(b)=\int_{\mathcal Z}\sum_{d=1}^{D}w_d \bigl(p_{c,t}(d,z;b)-\bar p_{c,t}(z;b)\bigr)^2\,\mathrm d\nu(z), \tag{7}

where () is a fixed probability distribution over a common calibrated range (Z). The equation is a proposed operational measure, not an established measurement of contemporary scientific AI. It is meaningful only when the task families and difficulty strata are sufficiently comparable and consistently sampled.

A decrease in the dispersion statistic Equation 7 does not by itself establish progress. Dispersion is zero when every domain fails, as well as when every domain succeeds. Progressive flattening therefore requires a joint statement: increasing mean performance, reduced difficulty-matched dispersion, and improvements in the weak-performing tail. A reduction in variance caused by deterioration of a previously strong domain would not count as desirable convergence. Nor would saturation on an easy benchmark establish reliable generality on tasks beyond its scope.

Local task irregularity requires a separate measure. Two domains can have equal average success while each contains unexpected pockets of failure. One approach fits an expected success function (m_t(z(x))) using task-level descriptors and measures the residual dispersion (E_). The meaning of this statistic depends on the specification of (m_t) and on whether the descriptors adequately capture relevant difficulty. It is best interpreted as conditional unpredictability within the chosen ontology, not an intrinsic geometry of intelligence.

Workflow reliability creates a further complication. If a research project requires a sequence of mandatory successful stages (E_1,,E_n), then the exact chain rule gives

\Pr\!\left(\bigcap_{i=1}^nE_i\right) =\prod_{i=1}^n\Pr\!\left(E_i\mid\bigcap_{j<i}E_j\right). \tag{8}

No independence assumption is needed. Even conditional success probabilities of 0.95 at ten mandatory stages imply approximately 0.60 end-to-end success if each stage retains that conditional probability. Repairs, checks, and retries can improve the resulting reliability, but they also consume resources and modify the process under evaluation. Excellent performance on isolated steps cannot therefore be substituted for demonstrated reliability on complete investigations.

A second limitation concerns the availability of valid feedback. Formal mathematical tasks can often provide exact deductive checking; software tasks support execution, testing, or selected formal guarantees; physics and chemistry may require numerical models; and experimental research ultimately depends on physical measurements whose uncertainty cannot be removed by logical proof. The effectiveness of agentic search may therefore increase disproportionately in tasks whose candidate outputs can be checked quickly and reliably.

Existing measurements illustrate the problem rather than settle it. METR’s January 2026 Time Horizon 1.1 revision expanded its task suite from 170 to 228, increasing coverage of longer tasks while warning that estimates remained sensitive to task selection and that uncertainty at the highest time horizons was substantial. A study of the SciCode benchmark reported extensive grading and specification defects that had incorrectly rejected many otherwise valid scientific-programming solutions.²²²³

These findings expose a danger in the apparent geometry of the frontier: jaggedness may originate partly in measurement artifacts. Conversely, an evaluation concentrated on easily verifiable tasks may make performance appear more uniform than it would on the broader population of scientific research. The relevant unit is the full performance surface indexed by task, resource allocation, verification regime, and system configuration—not a single benchmark score.

From mathematical proofs to verified executables: AlphaProof Code

The extension of AI-assisted formalization from mathematical theorems to compiled software reveals a deeper continuity. A proof assistant can verify a statement about abstract mathematical objects, but computation itself is also describable mathematically through programming-language semantics, transition systems, trace relations, and program logics. Formal software verification uses these descriptions to establish that computational artifacts satisfy properties expressed as mathematical propositions.

The objects differ, even if the logic is shared. Formalizing an existing theorem asks whether a proof term establishes the intended mathematical proposition. Verifying software asks whether an executable’s modeled behavior satisfies a specification; validating the result additionally requires confidence that the specification captures the intended operational requirement. Connecting the two activities is consequently more demanding than merely reusing a theorem prover.

Google DeepMind’s AlphaProof Code, announced on November 10, 2026, demonstrates an ambitious instance of this connection. Researchers employed human-guided specification agents, autonomous proof-generating agents, Lean, and a formal semantics of AArch64 Linux to establish selected security properties of a compiled libsignal implementation. The verified target was a small command-line program linked to unmodified Rust protocol crates and compiled through a stock rustc toolchain, rather than an entire deployed Signal application.²⁴

The technical paper reports about 6.5 million lines of generated Lean proofs resting on approximately 26,000 lines of trusted specification and machine semantics. It examines a particular AArch64 executable and selected protocol operations, including session initiation, message encryption, and decryption, with explicit contracts for external routines and assumptions about cryptographic primitives. The proof is thus connected to concrete binary bytes, but it is not a theorem about every platform, build configuration, operating-system behavior, or cryptographic implementation.

A generic executable-refinement property can be written as

\forall x\in\mathcal I,\quad \operatorname{Pre}(x)\Longrightarrow \operatorname{Traces}_{\mathcal E}(B,x) \subseteq\operatorname{Allowed}_S(x), \tag{9}

where (B) is a specific binary, (I) its admissible inputs, (E) a formal execution environment, and (_S) the behaviors permitted by specification (S). The relation is an explanatory trace-refinement model, not a verbatim restatement of the AlphaProof Code cryptographic theorems. Cryptographic confidentiality and noninterference may require relational or probabilistic properties that compare multiple executions rather than constraining one trace in isolation.

The result reported in the AlphaProof Code technical paper combines two security frameworks. The symbolic development treats cryptographic primitives through idealized operations in an adversarial protocol model, and the computational development bounds specified adversarial advantages by reductions to cryptographic assumptions. The paper establishes authentication, confidentiality-related guarantees, forward secrecy, post-compromise security, and qualified handshake-secrecy results, under different assumptions in each framework. Its computational guarantee concerns classical attackers; the symbolic analysis permits a particular abstraction of future quantum capabilities. These should not be merged into a claim of unconditional post-quantum security.²⁵

The architectural innovation is as important as the proof volume. Human-reviewed specifications are fixed as a baseline before agent proof construction. A gatekeeper uses the Lean kernel and a comparator to ensure that agents establish exactly the approved target rather than a weakened theorem whose dependencies have changed. The project also uses non-vacuity checks, adversarial review, mutation testing, and formal counterexamples involving two historical libsignal bugs. These tests give concrete evidence that the formal properties can distinguish certain defective implementations; they do not establish completeness against all possible vulnerabilities.

The assurance boundary in Figure 3 is therefore not the proof term alone. It includes source-to-specification interpretation, the faithful representation of machine execution, the trusted contracts, and the connection between modeled and real runtime environments.

%%{init: {"theme": "neo", "look": "handDrawn", "layout": "elk"}}%%
flowchart TB
    A[Human security objectives] --> B(Specification validation)
    B --> C[(Approved Lean specification)]
    D[(Unmodified Rust implementation)] --> E(Ordinary compilation)
    E --> F[(AArch64 executable)]
    F --> G(Formal machine semantics)
    H[(Trusted cryptographic contracts)] -.->|constrains| G
    C --> I(Agent proof construction)
    G --> I
    I --> J{Kernel and comparator accept?}
    C -.->|held-out baseline| J
    J -->|yes| K[(Machine-checked artifact)]
    J -->|no| I
    L[Human security review] -.->|approves meaning| C
    M[Actual deployment environment] -.->|requires fidelity argument| G

Figure 3: AI-generated software proofs reduce deductive labor, but their meaning depends on reviewed specifications, trusted machine semantics, and scope-limited assumptions about real execution.

The logical structure of the remaining problem is simple but consequential. If the verified behaviors of a program lie within the behaviors permitted by formal specification (S), and (S) itself is sufficiently restrictive to meet stakeholder requirements (R), then both links support the intended assurance claim. In a common behavioral domain, a sufficient relationship for the latter link is

\operatorname{Allowed}_S\subseteq\operatorname{Allowed}_R. \tag{10}

Proving the first relationship does not prove the second. The hard-to-automate activity may increasingly be specifying the right property, reviewing the trusted computing base, and maintaining correspondence with a changing executable rather than generating the millions of deductive proof steps.

AlphaProof Code also belongs in a longer history. CompCert formally established semantic preservation for a substantial C compiler, and seL4 developed machine-checked relationships among operating-system specifications and implementations. The novelty is not that mathematics was first applied to software in 2026, but that AI-assisted proof construction was applied at considerable scale to selected security properties of a preexisting, widely used cryptographic implementation.²⁶²⁷

This is a consequential spillover from mathematical AI. Formal mathematics supplies the logical language for reasoning about computation; verified software can supply stronger components for subsequent scientific computation. The two converge in their proof infrastructure, even while the semantic and physical assumptions surrounding them remain distinct.

From mathematics to computer science, theoretical physics, and experimental science

Transfer from mathematics into other sciences cannot be inferred solely from the appearance of mathematical symbols in their publications. The relevant issue is whether the same computational mechanisms support investigations whose final claims require different evidence. An algorithmic theorem can often be established deductively; a theoretical physics calculation is valid within its model; a chemical hypothesis generally requires measurement. These activities may share reasoning and tool infrastructures without sharing acceptance criteria.

Theoretical computer science offers the closest connection. Google’s November 13 report describes AI-assisted results in quantum query complexity, graph sparsification, Boolean matrix multiplication, sparse embeddings, and information theory, with several arguments formalized in Lean. A result about quantum query complexity concerns an abstract oracle model; it does not mean that a physical quantum processor has executed the algorithm. Likewise, a proof of a streaming-algorithm bound says something about specified memory, update, and approximation guarantees, not automatically about performance in every deployed system.²⁸

In mathematical physics the gap becomes more visible. OpenAI’s February work on single-minus gluon scattering amplitudes involved identifying an unexpectedly simple expression in a special half-collinear regime and checking it against relevant recursion identities and soft limits. Its September Navier–Stokes result concerned a forced singularity in a continuum equation, not the direct observation of a physical fluid moving at infinite speed. Anthropic’s November preprints on the Hawking–Page transition and the modular bootstrap likewise provide sophisticated mathematical analyses of theoretical models, rather than new measurements of black holes or quantum gravity.²⁹³⁰

The key mechanism is verifiability. An agent searching through candidate derivations can receive strong feedback from algebraic identities, numerical consistency checks, or proof assistants. It cannot obtain empirical validation of a physical theory merely from the deductive consistency of the theory’s equations. Physical relevance requires additional evidence about the relation between model and world.

Experimental chemistry demonstrates another step. Google reported an Antigravity workflow that used 30 specialized agents and a physics-informed simulator to identify molecular structures from nuclear magnetic resonance data, with 95% top-one and 100% top-three accuracy on its selected benchmark. This is an inverse problem constrained by experimental observations and a computational spectral model, not evidence that the system had synthesized or biologically validated the molecules.³¹

By contrast, OpenAI’s collaboration with Molecule.one connected a model to an automated chemistry platform and measured the effects of proposed changes to a Chan–Lam reaction class. More than 10,000 reactions were reportedly tested; yields improved for substantial shares of the tested substrate classes, and a subset of reactions was replicated at bench scale. The resulting evidence concerns real chemical measurements under defined experimental conditions. It does not establish the reaction’s universality across every substrate, laboratory, or scale.³²

A collaboration with Ginkgo Bioworks reported reduced costs of cell-free protein synthesis through repeated automated experiments. The result concerns a specified reaction system and protein, and its transfer to different proteins or production geometries remains uncertain. Similarly, autonomous materials work such as SARA-H connects probabilistic experimental planning with robotic synthesis and physical characterization; its contribution depends on successful production and measurement, not on a language-model response alone.³³³⁴

The difference can be modeled through an inverse scientific problem. Let (M) be a hypothesized molecular structure, () experimental conditions, (g) a forward spectral model, (y) observed measurements, and () measurement and model error:

y=g(M,\theta)+\varepsilon. \tag{11}

Recovering (M) from (y) may be underdetermined when several structures produce spectra indistinguishable within experimental precision. A powerful reasoning system can rank candidates and propose discriminating experiments, but it cannot infer information absent from the observations without additional assumptions.

Recent biological work similarly spans prediction and validation. Anthropic reported computational reconstruction of certain adeno-associated viral capsids using multiple folding models and symmetry information, while Google introduced a cell-context-conditioned genomic model intended to predict effects of sequence variation. Predictive improvements can help identify candidate mechanisms; they do not on their own establish causality, therapeutic performance, or cellular behavior across untested environments.³⁵³⁶

The strongest warning against premature generalization comes from routine tasks. OpenAI’s BioBasicsBench evaluates interpretation of raw laboratory materials, including gels, microscopy, and instrument readings. GPT-6 Astra scored 66.7% mean reward at the reported xhigh setting, compared with 43.8% for GPT-5.6 Sol, with failures remaining in ordinary scientific evidence interpretation. These percentages are rubric-based mean rewards, not probabilities of completing a research project. Their significance is that extraordinary mathematical results can coexist with imperfect performance on mundane operations essential to scientific inference.³⁷

The differences are summarized in Table 2.

Research regime	Primary acceptance evidence	Residual boundary
Formal mathematics	Kernel-checked proof and semantic review	Meaning, axioms, novelty
Formal software assurance	Refinement proof for specified executable properties	Adequacy of requirements and execution model
Theoretical physics	Analytical derivation and model checks	Physical applicability
Computational chemistry and biology	Predictive benchmarks and numerical validation	Model discrepancy, biological function
Laboratory science	Instrumental observations, controls, replication	Confounding, generalization, reproducibility
Historical mathematical reconstruction	Source provenance and checked reconstruction	Attribution, authorship, interpretive fidelity

Table 2: Distinct types of scientific evidence encountered by AI-assisted research systems.

The comparison supports the conclusion that a common computational substrate—symbolic reasoning, code, simulation, tool invocation, and iterative evaluation—does not provide one automatically transferable guarantee of scientific correctness. The frontier may be flattening within tasks equipped with strong feedback while remaining uneven across complete investigations constrained by experiments, identification, and interpretation.

Reconstructing mathematical knowledge: AI and Gödel’s notebooks

A scientific discovery can enlarge usable knowledge without establishing a theorem that was previously unknown to mathematics. Unpublished notebooks, correspondence, unfinished proofs, and abandoned research programs may preserve results and methods that never entered the working literature. Their recovery changes what later investigators can access and reuse. AI-assisted reconstruction of such material is therefore a distinct mode of research, not merely a variant of proof search.

The University of Helsinki’s Gödel Enigma project has spent years transcribing and interpreting the extensive manuscripts of Kurt Gödel, many written in Gabelsberger shorthand. Its work predates modern generative AI and has already produced scholarly reconstructions of Gödel’s unpublished foundational research. The source corpus is not a database of finished theorems: it contains provisional definitions, marginal corrections, false starts, and arguments whose premises are distributed across different notebooks.³⁸

In November 2026, Jan von Plato reported using Claude to interpret transcriptions of approximately 1,009 pages of Gödel’s workbooks alongside his own studies and other historical material. In an interview, he described receiving a 650-page synthesis, extracting 663 candidate theorem statements, and checking or repairing many of them with Coq. He gave approximate counts of 400 statements verified as written, 200 repaired, and 50 false; these rounded categories do not exhaustively reconcile to the reported 663. The interview did not supply a public theorem-by-theorem corpus or the complete formal artifacts needed for an independent audit.³⁹

The distinction between transcription and reasoning must be retained. Claude reportedly worked on specialist-produced textual transcriptions, not on 1,009 manuscript images that it had independently deciphered. The human preprocessing was an indispensable part of the research process. The model’s reported contribution was to integrate mathematical context across a large textual corpus, connect distributed definitions, propose interpretations, and help reconstruct proof obligations.

The strongest historical claim concerns a possible route to the independence of the axiom of choice. Two mathematical statements must be separated. Gödel’s constructible-universe method established the relative consistency of choice with Zermelo–Fraenkel set theory, while Cohen later established the relative consistency of the negation of choice by developing forcing. In standard metamathematical notation these are, respectively,

\operatorname{Con}(\mathrm{ZF})\Longrightarrow \operatorname{Con}(\mathrm{ZF}+\mathrm{AC}), \tag{12}

and

\operatorname{Con}(\mathrm{ZF})\Longrightarrow \operatorname{Con}(\mathrm{ZF}+\neg\mathrm{AC}). \tag{13}

These are different results. The report suggests that Gödel had approached an argument related to the second direction and that a defect in one definition could be repaired using other manuscript material. But a valid modern Coq proof of a related proposition would not automatically establish that Gödel possessed that completed proof or that its exact formal theory was the standard ZF framework. Gödel’s own correspondence distinguishes some of his earlier partial independence investigations in type theory from Cohen’s approach. A reliable historical conclusion requires manuscript passages, exact theorem statements, chronology, and explicit attribution of the steps supplied by modern investigators.⁴⁰

Three questions must therefore remain separate: is the reconstructed proposition mathematically true; is it a faithful interpretation of the manuscript; and did the historical author establish or understand the proof now presented? A proof assistant can answer the first relative to an accepted formalization, but not the other two. Adding an assumption to make a false statement correct may yield new mathematics without preserving the content of the original note.

As Figure 4 makes explicit, a rigorous research archive needs two connected evidentiary chains: source-to-claim provenance and claim-to-proof validity.

%%{init: {"theme": "neo", "look": "handDrawn", "layout": "elk"}}%%
flowchart TB
    A[(Original notebooks)] --> B(Specialist transcription)
    B --> C(AI-assisted reconstruction)
    C --> D[(Candidates with page mappings)]
    D --> E(Historical interpretation review)
    D --> F(Formal statement and proof attempt)
    F --> G{Proof checker accepts?}
    G -->|no| H[(Unresolved or false obligations)]
    H -->|reformulates with provenance| F
    G -->|yes| I[(Formal proof evidence)]
    E --> J(Integrate distinct evidence)
    I --> J
    J --> K[(Versioned mathematical archive)]
    A -.->|constrains attribution| E

Figure 4: Historical attribution and mathematical validity are different evidence chains; formally repairing a claim does not establish that the historical author held the repaired result.

The case has implications beyond Gödel. A mathematical archive may contain valid unpublished results, incomplete approaches to later discoveries, alternative techniques that become useful with modern methods, and false conjectures whose examination reveals meaningful conceptual structure. The value of AI lies partly in making large-scale relationships across such material navigable, provided original sources and uncertainty remain visible.

Formal mathematical infrastructure and historical reconstruction could become complementary. The latter identifies candidate mathematical objects and reconstructs their intended meanings; the former attempts to represent and verify those objects in reusable libraries. The result could enlarge the effective stock of knowledge even where the underlying truth was not new. This is a promising direction, but the 2026 Gödel claims remain preliminary until the reconstructed statements and proof artifacts are independently available for inspection.

Why a flatter frontier does not imply uniform scientific competence

Some sources of uneven capability are contingent engineering weaknesses; others arise from the logic of inference itself. The difference is important. Better models and tools can reduce many observed errors, but they cannot turn an underdetermined scientific question into one with a uniquely justified answer when the necessary evidence is absent. Nor can any effective general procedure decide every sufficiently expressive computational or logical problem. These are limits on universal decision procedures and identification from incomplete information, not predictions that progress on particular research distributions must stop.⁴¹

The semantic gap is a recurring source of error. A formal proof may be valid but concern a weakened theorem. A software model may omit a relevant attack scenario. A numerical simulation may be internally consistent but inaccurate for the physical regime under investigation. A historical reconstruction may prove a proposition that the original author did not intend. In each case, verification of a representation does not automatically validate its correspondence with the target of inquiry.

Scientific inference can also be unidentifiable. Consider two structural causal models with a fair binary exogenous variable (U). In one, (X=U) and (Y=X); in the other, (Y=U) and (X=Y). Both generate the observational distribution ((X=Y=0)=(X=Y=1)=1/2), yet intervening to set (X=1) gives different predictions:

\Pr_1(Y=1\mid\operatorname{do}(X=1))=1, \qquad \Pr_2(Y=1\mid\operatorname{do}(X=1))=\tfrac12. \tag{14}

The common observational distribution alone does not identify the correct interventional conclusion; extra causal assumptions or interventional evidence are required. An AI system may help design a discriminating experiment, but it cannot recover information that the data do not contain.⁴²

The reliability of many-agent systems likewise depends on the correlation of their mistakes. Let (E_i) be a binary error indicator for reviewer (i), with common error probability (p) and pairwise correlation (). For (m) reviewers,

\operatorname{Var}\!\left(\frac1m\sum_{i=1}^{m}E_i\right) =\frac{p(1-p)}{m}\bigl[1+(m-1)\rho\bigr]. \tag{15}

If errors are independent, the variance decreases with reviewer count. With persistent positive correlation, a common-mode component remains even as the team grows. This is a statement about variance, not a universal majority-vote failure rate; nevertheless it explains why several agents sharing a flawed specification, retrieved reference, or implicit assumption need not constitute independent scientific review.

Human involvement is not automatically an independent safeguard. An October 2026 experiment with experienced analysts found that assigned preferences expressed by AI agents influenced many methodological choices, even when multiple choices were defensible. The study’s limited setting does not quantify the effect in all research fields, but it establishes why a human signature alone cannot be taken as proof of independent evaluation.⁴³

Physical constraints create another source of persistent disparity. Under a simple sequential workflow model, if a fraction (q) of completion time is unaffected by automation while the remaining fraction is accelerated by factor (s), then the overall speedup satisfies

S\leq\frac{1}{q+(1-q)/s}. \tag{16}

This is Amdahl’s law under specified assumptions, not a universal ceiling on scientific progress: research procedures and experiments can be redesigned. It does, however, clarify why faster reasoning may yield dramatically different gains in computational mathematics and in a laboratory constrained by incubation, instrument occupancy, safety procedures, or physical sample preparation.

Benchmark defects can also imitate the jaggedness being measured. A system may be penalized for a valid scientific answer when a reference implementation or numerical tolerance is wrong; conversely, contaminated or permissive tasks may overstate capability. The SciCode-Verified audit and subsequent benchmark corrections show that evaluation error is an empirical variable rather than a theoretical afterthought.⁴⁴

Finally, model-level performance and complete-workflow productivity need not move together. METR’s 2025 randomized study found a slowdown for experienced developers using then-available AI tools on a selected set of real issues, while its 2026 follow-up reported suggestive but methodologically uncertain evidence of improvement. These findings cannot be generalized to all software work, but they warn against replacing measured completion cost with subjective impressions or isolated benchmark gains.⁴⁵⁴⁶

The strongest inference is conditional: capability may converge locally among tasks with explicit representations and reliable checkers, while scientific reliability remains uneven where requirements are ambiguous, observations are underdetermined, experiments are expensive, or evaluators share systematic errors. This does not negate the achievements of AI-assisted research; it identifies the parts of scientific competence that a convincing generality claim must still measure.

The emerging economics and organization of computational discovery

Lowering the cost of producing candidate proofs and scientific hypotheses changes research incentives, but the final output of science is not candidate volume. An accepted contribution requires correctness, novelty assessment, interpretation, reproducibility where applicable, and integration into an accessible knowledge record. If the cost of generating plausible research artifacts declines faster than the cost of evaluating them, scarcity shifts toward verification and expert attention.

This transition connects two established economic observations. Jones’s burden of knowledge argument links scientific accumulation with greater specialization and collaborative organization. Bloom, Jones, Van Reenen, and Webb document settings in which maintaining research progress required increasing effort. Neither result is a universal law about future AI productivity, but both explain why more researchers, manuscripts, or agent executions are insufficient measures of cumulative discovery.⁴⁷⁴⁸

A simple queueing model makes the new bottleneck explicit. Let (_g) be the rate of candidate-generation, let a screening process admit a fraction (a) for detailed review, and let (_v) be the verification service rate. Then (_v=a_g) is the arrival rate of claims awaiting review. Under an illustrative single-server (M/M/1) model with Poisson arrivals and exponentially distributed service times, expected time in the verification system is

W_v=\frac{1}{\mu_v-\lambda_v},\qquad \lambda_v<\mu_v. \tag{17}

Scientific review does not literally operate as one memoryless server; manuscripts differ in difficulty and receive multiple review rounds. The model nevertheless demonstrates a structural consequence: delay can increase disproportionately as admitted submission rates approach effective capacity. In October 2026 Finland’s Publication Forum mathematics panel issued a preliminary warning about growing submission volume and scarce expert review. It explicitly lacked a statistically rigorous survey, so its concerns should be treated as an institutional observation rather than a quantitative estimate of AI’s causal contribution.⁴⁹

A November theoretical economics preprint examines another possible mechanism. When manuscript production becomes cheap, the size or polish of a submission may convey less information about underlying research quality. Under specified assumptions about asymmetric information, screening, and voluntary review effort, a reduction in production costs can even lower the equilibrium quantity of verified knowledge. This is a conditional model, not evidence that global scientific output has already declined.⁵⁰

Formal proof systems offer a partial counterweight because they can lower deductive checking costs. The crucial qualification is that checking the proof is not the same as reviewing the theorem statement, foundational definitions, novelty, or scientific importance. As the cost of proof generation falls, semantic assurance may become a larger share of the total validation burden.

Reusable mathematical libraries can improve this allocation by allowing foundational verification to serve many investigations. Suppose (n) projects have stand-alone formalization costs (b_i). A shared library costs (F) to create and introduces incremental formalization and maintenance costs (r_i) and (m_i) per project. The shared investment breaks even under the simplified accounting condition

F+\sum_{i=1}^{n}(r_i+m_i)<\sum_{i=1}^{n}b_i. \tag{18}

The inequality supplies no numerical estimate of Axiom’s performance; its point is to distinguish a one-off proof from a reusable foundation. An extensible library can compound returns across future investigations if its abstractions are semantically valid, its interfaces remain compatible, and independent researchers can access it. Otherwise, large generated libraries can simply create expensive maintenance obligations.

Research harnesses likewise raise organizational questions. Parallel research agents incur task-specification, communication, integration, and verification costs. Central orchestration can reduce inconsistency but become a bottleneck; decentralized exploration can increase diversity but duplicate work or propagate incompatible assumptions. Coase’s transaction-cost account of the firm provides an analogy rather than a direct theorem about AI laboratories: the choice of coordination structure depends on the relative costs of arranging, monitoring, and integrating work.⁵¹

Institutions are adapting to the resulting tension between commercial discovery and scholarly evaluation. The September 2026 mathematical declaration on AI warned that prestige-driven conjecture solving could divert attention from durable understanding. An independent advisory group recommended prompt publication of otherwise inaccessible mathematical results, transparent provenance, and community-led interpretation. In October, the Simons Foundation, Anthropic, and OpenAI announced $15 million in combined funding and resources for mathematics-related evaluation and adaptation. These are responses to the verification and governance problem, not evidence that it has been solved.⁵²⁵³⁵⁴

The allocation of scientific authority is central. A company may possess the infrastructure that produces a result, while the broader community supplies the specialist knowledge required to judge its meaning. Restricted access to unpublished proofs, proprietary models, and large inference budgets can concentrate research opportunity; open mathematical libraries can lower some barriers while leaving compute and experimental resources scarce. The relevant question is not whether companies can make valuable discoveries, but how discovery, independent examination, publication, and attribution should be organized when their costs and incentives diverge.

A productive research system should therefore be judged by validated knowledge yield rather than the number of candidate outputs. Its economics include inference, rejected attempts, formal checking, expert interpretation, physical experiments, repository maintenance, and the opportunity cost of scientific attention. An organization that makes hypothesis generation cheap but leaves those costs external to itself has not necessarily made science cheaper overall.

How to measure scientific convergence rather than assume it

A credible test of global frontier flattening requires a stable target population and a protocol whose changes can be distinguished from changes in the evaluated systems. The tasks must cover different disciplines and epistemic regimes, including mathematical discovery, formalization, software verification, numerical modeling, empirical data interpretation, experimental investigation, and historical reconstruction. Domain labels alone are insufficient: algorithm verification and formal mathematics may share more relevant mechanisms than computational chemistry and physical chemical synthesis, despite the latter belonging to one discipline.

The evaluation should preserve two strata: scientific domain and operational task mechanism. It should separately record novelty, task ambiguity, available feedback, required scientific tools, calibrated difficulty, and the extent of methodological guidance. Existing-knowledge retrieval should not be scored as genuinely new mathematical discovery, and completion of a detailed replication protocol should not be conflated with independently selecting a scientific method.

Available benchmarks are informative but partial. FrontierMath assesses difficult mathematical reasoning with checkable answers; FrontierMath Open Problems aims at research questions whose answers were unknown at inclusion. RE-Bench measures research-engineering tasks against human baselines, while PaperBench assesses replication of existing AI research through detailed rubrics. ASI-Bench evaluates project-level tasks across disciplines and examines performance as methodological guidance is withdrawn. None can by itself estimate reliable general scientific competence.^55565758

Benchmark integrity requires version control. In June 2026 Epoch revised FrontierMath after correcting problems affecting 42% of the original set, illustrating why raw scores across benchmark versions are not automatically comparable. METR’s time-horizon revisions likewise changed task composition and shifted estimates even without changes in the systems being evaluated. Reliable longitudinal inference requires frozen anchor tasks, documented changes to graders, overlapping reevaluation of old and new systems where feasible, and explicit uncertainty for comparisons across revised instruments.⁵⁹⁶⁰

Research-system components should also be separated experimentally. In a simple factorial design, evaluate two models (M_0,M_1) with two harnesses (H_0,H_1), producing the configurations ((M_0,H_0)), ((M_1,H_0)), ((M_0,H_1)), and ((M_1,H_1)). This can distinguish model effects, harness effects, and their interaction under matched resource and task conditions. Where proprietary systems prevent such cross-combinations, the study should identify the comparison as system-level rather than attributing the difference to the model alone.

Resource normalization must include more than tokens. Wall-clock duration, aggregate inference expenditure, hardware, tool access, human intervention, formal-verification work, laboratory instruments, and the reuse of prior formal knowledge can each change the result. A descriptive incremental cost per independently validated output is

C_{\mathrm{valid}}=\frac{C_{\mathrm{all}}}{N_{\mathrm{valid}}}, \qquad N_{\mathrm{valid}}>0, \tag{19}

where (C_{}) includes generation, failures, tool execution, human labor, and validation under a declared accounting convention. The measure does not capture scientific importance and is undefined when no result is validated; it should be reported alongside, rather than substituted for, measures of novelty and utility.

Repeated attempts are necessary to estimate reliability, but trials on the same task are correlated. A hierarchical logistic model could represent a binary success outcome (Y_{i,r,c,t}) for trial (r) on task (i) as

\operatorname{logit}\Pr(Y_{i,r,c,t}=1) =\alpha_{d(i),c,t}+u_{f(i)}+v_i+\beta^\top x_i, \tag{20}

where (d(i)) is the scientific domain, (f(i)) a task family, (u_{f(i)}) and (v_i) family and task effects, and (x_i) prespecified task descriptors. The formulation is illustrative; estimation should be adapted to the data and should propagate uncertainty into nonlinear dispersion measures. Treating many attempts on one theorem as many independent theorems would exaggerate precision.

Complete research workflows require separate outcomes. A proof that typechecks may await semantic review; a laboratory observation may await replication; a historical theorem reconstruction may be mathematically valid but disputed in attribution. A study should distinguish confirmed success, confirmed failure, and unresolved validation rather than prematurely treating every pending claim as a success or failure. Scientific novelty and longer-term utility also deserve separate assessment: immediate correctness is not a measure of eventual influence.

The empirical protocol can be summarized without inventing one universal scientific score. Define the task population and its sampling weights in advance; audit and version task specifications; evaluate models and harnesses under matched conditions; collect repeated outcomes; validate each result using an appropriate independent method; estimate mean capability, conditional jaggedness, and lower-tail reliability; and preserve economic costs and durable artifact provenance. A standing scientific-frontier observatory would be better suited to this work than a one-time leaderboard.

Persuasive evidence of flattening would show stronger performance in previously weak task families, declining conditional disparities at comparable difficulty, gains that persist outside familiar benchmarks, less dependence on supplied research strategies, and greater end-to-end reliability under independent validation. The hypothesis would be weakened if progress remained concentrated in easily formalizable tasks, if the lower tail remained poor, or if model gains failed to survive complete-workflow evaluation. The evidence may support local convergence without supporting a global claim, and that intermediate conclusion should be reported rather than forced into a binary verdict.

Conclusion: from mathematical intelligence to scientific infrastructure

The most important development of 2026 is not the resolution of one famous conjecture, nor the production of the largest formal proof repository. It is the growing ability to combine fallible reasoning models with specialized verification, persistent mathematical knowledge, executable scientific tools, and research workflows that preserve intermediate evidence. The emerging capability is organizational and computational as well as cognitive.

The evidence supports a substantial expansion of scientific AI. Competing laboratories have reported new mathematical arguments and formalizations, research-level results in algorithms and theoretical physics, selected properties of compiled software verified through formal semantics, and experimentally assessed improvements in chemistry and biology. The Axiom releases suggest that large mathematical theories can increasingly become reusable computational infrastructure, while the Gödel investigation suggests that AI may also enlarge the accessible stock of historical mathematical knowledge. These are distinct achievements, but they point toward a common infrastructure in which claims, proofs, models, programs, and experiments become more closely linked.

A strong claim about global flattening remains unestablished. Mathematical proof validity, semantic fidelity, software-specification adequacy, physical-model validity, causal identification, experimental reproducibility, and historical attribution are different epistemic obligations. A system that performs exceptionally on one may remain unreliable on another. The availability of exact formal checkers can make certain classes of research much more tractable, while ambiguous requirements and physical observation preserve discontinuities across complete scientific workflows.

The formal distinction is consequently decisive. A frontier that moves outward includes more tasks above a specified reliability threshold. A frontier that flattens exhibits smaller disparities among comparable classes, together with improvements in average and lower-tail capability. Existing 2026 results demonstrate the first and make some forms of the second plausible; they do not yet permit a controlled longitudinal estimate of the second.

The economic and institutional consequences may emerge before reliable generality. When candidate results become cheap, the allocation of expert attention, verification throughput, experimental access, and mathematical understanding becomes more consequential. Formalized knowledge can accumulate and reduce duplicated work, but only when definitions, dependencies, and source mappings are maintained. The authority to generate a result remains distinct from the authority to assess its scientific status. Research organizations therefore need arrangements in which independent interpretation and provenance scale alongside automated discovery.

The deeper possibility is a cumulative computational scientific system. Mathematical libraries would preserve formal results; verified software would support trustworthy parts of the computational stack; simulations would transform model assumptions into predictions; physical experiments would provide evidence that computation alone cannot supply; and historical reconstruction would recover ideas previously absent from the effective scientific record. None of those components abolishes the need to ask whether the underlying scientific question has been answered.

A decisive future milestone would therefore be more demanding than an additional spectacular theorem: a research system that repeatedly moves from an independently meaningful question to a validated result, with transparent resources, explicit assumptions, independently inspectable evidence, and durable knowledge available for later investigations. Such a demonstration would provide substantive evidence of increasingly general scientific competence rather than a further example of exceptional local performance.

AI’s scientific frontier is expanding; whether its jaggedness is declining remains an empirical question. The most important transformation already visible is the emergence of infrastructure capable of making scientific investigation more computational, verifiable, and cumulative—provided that the standards governing meaning, evidence, and scientific authority remain as rigorous as the systems that produce the results.

See also machine learning longforms

The Firm That Thinks: Company Brains, Agent Coworkers, and the Future of Organizational Autonomy

Toward a theory of organizational cognition, computational agency, and governable enterprise autonomy

What Kind of Thing Is an Alien Mind?

Reading Jakub Pachocki on intelligence, agency, alignment, opacity, and recursive self-improvement

AI Adoption, Productivity, and the Missing Middle

A review of Banca d'Italia QEF 1009 on Italy's AI adoption, firm productivity, and policy architecture

See also mathematics longforms

Homomorphic Encryption for Developers

From algebraic foundations and textbook RSA to practical BFV and dependable private computation

The Mathematics Behind a Racing Shell

Why rowing-boat simulation is a difficult multiphysics engineering problem

Sudoku and Satisfiability Modulo Theories

You can solve it the standard way or... with Python and math

See also posts

L'impresa che pensa: cervello aziendale, agenti-colleghi e valore dell'organizzazione

Come cambiano conoscenza, lavoro e responsabilità quando l'intelligenza artificiale entra nei processi aziendali

The Machines That Find the Flaws

Frontier AI, agentic cybersecurity operations, and the transition from vulnerability discovery to verifiable security

After the Enormous Theorem: Verification, Discovery, and the Missing Layer of Understanding

Axiom’s formalization, OpenAI and Anthropic’s discoveries, Yang–Mills scrutiny, and compute-allocable mathematics

Mistral and the European AI Frontier

How much technological sovereignty does model competitiveness buy?

Math 2.0 Gets an Operating System: Can Open Math OS Build Mathematics Beyond the Theorem Factory?

From mathematical AI agents to durable knowledge and independent research institutions

Math 2.0: Beyond the Theorem Factory

Terence Tao on proof abundance, mathematical understanding, and the redesign of research

Footnotes

1. Dell’Acqua, F., McFowland, E., Mollick, E. R., Lifshitz-Assaf, H., Kellogg, K. C., Rajendran, S., Krayer, L., Candelon, F., & Lakhani, K. R. (2023). Navigating the jagged technological frontier: Field experimental evidence of the effects of AI on knowledge worker productivity and quality. Harvard Business School Digital Data Design Institute. Research summary.

2. Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024). Solving olympiad geometry without human demonstrations. Nature, 625, 476–482. DOI.

3. Google DeepMind. (2025). Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad. Google DeepMind. Research announcement.

4. OpenAI. (2026, October 6). Sharing AI progress in mathematics. OpenAI. Research release. The report describes the public repository, included Lean formalizations, revision process, attempt statistics, and equivalent compute estimates; these disclosures should not be interpreted as independent validation of every mathematical claim.

5. OpenAI. (2026, October 26). Working with academic communities to build scientific understanding. OpenAI. Research announcement. Public release status and the company’s claims about ETH, local smoothing, and restricted quantum field theory material must be distinguished from independent community adjudication.

6. Anthropic. (2026, August 10). Learning more about Claude’s mathematical capabilities. Anthropic Research. Research report. The work concerns a lower bound for a fraction of zeros satisfying the hypothesis, not a proof of the Riemann hypothesis.

7. Anthropic. (2026, November 9). Introducing Claude Fable 5.2 and Claude Mythos 5.2. Anthropic. Research announcement. The announcement distinguishes formal mathematics, quantum field-theoretic preprints, and computational protein modeling, all of which require their own validation standards.

8. Luong, T., & Mirrokni, V. (2026, February 11). Accelerating mathematical and scientific discovery with Gemini Deep Think. Google DeepMind. Research report.

9. Google Antigravity. (2026, August 27). Teamwork: When AI becomes a research partner. Google Antigravity. Technical report.

10. Axiom Math. (2026, October 26). Formalizing the enormous theorem. Axiom Math. Technical research report. The organizational report describes a claimed complete Lean formalization and its mathematical repair process; independent reproduction remains a separate issue.

11. Axiom Math. (2026, November 4). The Stacks Project, formalized in Lean. Axiom Math. Technical research report.

12. OpenAI. (2026, October 26). Working with academic communities to build scientific understanding. OpenAI. Research announcement. Public release status and the company’s claims about ETH, local smoothing, and restricted quantum field theory material must be distinguished from independent community adjudication.

13. OpenAI. (2026, September 8). On the Navier–Stokes Millennium Prize Problem. OpenAI. Research publication. This is a company-released claimed resolution of specified smooth-forcing formulations; it should not be confused with independent prize adjudication.

14. Anthropic. (2026, August 10). Learning more about Claude’s mathematical capabilities. Anthropic Research. Research report. The work concerns a lower bound for a fraction of zeros satisfying the hypothesis, not a proof of the Riemann hypothesis.

15. Anthropic. (2026, November 9). Introducing Claude Fable 5.2 and Claude Mythos 5.2. Anthropic. Research announcement. The announcement distinguishes formal mathematics, quantum field-theoretic preprints, and computational protein modeling, all of which require their own validation standards.

16. Axiom Math. (2026, October 26). Formalizing the enormous theorem. Axiom Math. Technical research report. The organizational report describes a claimed complete Lean formalization and its mathematical repair process; independent reproduction remains a separate issue.

17. Axiom Math. (2026, November 4). The Stacks Project, formalized in Lean. Axiom Math. Technical research report.

18. Axiom Math. (2026, November 6). The Weil conjectures, formalized in Lean. Axiom Math. Technical research report.

19. Axiom Math. (2026, November 12). Faltings’ theorem formalized. Axiom Math. Technical research report.

20. Lin, H., Woodruff, D. P., Deng, Y., Mao, J., Zuo, S., & Mirrokni, V. (2026). Stellar Colosseum: A many-agent harness for long-horizon research in mathematics and theoretical computer science. arXiv. Preprint.

21. Mirrokni, V. (2026, November 13). Advancing science and engineering with Antigravity’s /teamwork. Google Research. Research report. The research page contains model and agent-system claims, formalization examples, computational benchmarks, and reported scientific outcomes with heterogeneous validation.

22. METR. (2026, January 29). Time Horizon 1.1. METR. Evaluation methodology. The task suite grew to 228 tasks, but its authors stress benchmark-composition sensitivity and wide confidence intervals.

23. Hu, S., Huang, L., Deng, Y., & Chen, K. (2026). SciCode-Verified: How benchmark defects underestimated the scientific-coding ability of language models. arXiv. Preprint.

24. Chaudhuri, S., Ferraiuolo, A., Kovsharov, A., Chajed, T., Schlesinger, S., Seth, K., Katz, J., Sutton, C., & Kohli, P. (2026, November 10). AlphaProof Code: Verifying Signal’s security at the machine-code level. Google DeepMind. Technical paper and interactive source. See also Google DeepMind. (2026, November 10). Introducing AlphaProof Code: A breakthrough in verifying complex software at depth. Google DeepMind. Research announcement.

25. Chaudhuri, S., Ferraiuolo, A., Kovsharov, A., Chajed, T., Schlesinger, S., Seth, K., Katz, J., Sutton, C., & Kohli, P. (2026, November 10). AlphaProof Code: Verifying Signal’s security at the machine-code level. Google DeepMind. Technical paper and interactive source. See also Google DeepMind. (2026, November 10). Introducing AlphaProof Code: A breakthrough in verifying complex software at depth. Google DeepMind. Research announcement.

26. The CompCert Project. (2026). The CompCert verified C compiler: Commented formal development. CompCert. Technical documentation.

27. seL4 Foundation. (2026). seL4 proofs: Functional correctness, binary correctness, and security. seL4. Formal verification documentation.

28. Mirrokni, V. (2026, November 13). Advancing science and engineering with Antigravity’s /teamwork. Google Research. Research report. The research page contains model and agent-system claims, formalization examples, computational benchmarks, and reported scientific outcomes with heterogeneous validation.

29. Lupsasca, A. (2026, February 13). GPT-5.2 derives a new result in theoretical physics. OpenAI. Research report.

30. Anthropic. (2026, November 9). Introducing Claude Fable 5.2 and Claude Mythos 5.2. Anthropic. Research announcement. The announcement distinguishes formal mathematics, quantum field-theoretic preprints, and computational protein modeling, all of which require their own validation standards.

31. Mirrokni, V. (2026, November 13). Advancing science and engineering with Antigravity’s /teamwork. Google Research. Research report. The research page contains model and agent-system claims, formalization examples, computational benchmarks, and reported scientific outcomes with heterogeneous validation.

32. OpenAI. (2026, June 17). A near-autonomous AI chemist improves a challenging reaction in medicinal chemistry. OpenAI. Experimental research report.

33. OpenAI. (2026, February 5). GPT-5 lowers the cost of cell-free protein synthesis. OpenAI. Experimental research report.

34. Chang, M.-C., Amsler, M., Sutherland, D. R., Ament, S., Gann, K. R., Zhou, L., Smieska, L. M., Woll, A. R., Gregoire, J. M., Gomes, C. P., van Dover, R. B., & Thompson, M. O. (2026). Autonomous materials exploration integrates automated phase identification and AI agents enhanced by human guidance. PRX Intelligence, 1, 013019. DOI.

35. Anthropic. (2026, November 9). Introducing Claude Fable 5.2 and Claude Mythos 5.2. Anthropic. Research announcement. The announcement distinguishes formal mathematics, quantum field-theoretic preprints, and computational protein modeling, all of which require their own validation standards.

36. Gayoso, A., Latysheva, N., Kohli, P., & Avsec, Ž. (2026, November 11). AlphaGenome 2: Deciphering how cells read DNA to better understand disease. Google DeepMind. Research announcement.

37. OpenAI. (2026, November 6). Measuring how AI agents handle everyday wet-lab science. OpenAI. Benchmark report. The reported percentages are mean rubric rewards for repeated trials, not general task-completion probabilities.

38. University of Helsinki. (n.d.). Gödel Enigma: Project description. University of Helsinki. Project documentation.

39. Bellos, A. (2026, November 13). ‘Ahead of his time’: AI helps unlock discoveries hidden in notebooks of man who transformed maths. The Guardian. Interview and original reporting. The theorem counts and claimed Coq outcomes are attributed to von Plato and were not accompanied by a public theorem-level audit.

40. Gödel, K. (1967, June 30). Letter to Wolfgang Rautenberg. In Kurt Gödel: Collected Works, Volume V: Correspondence H–Z (2003). Oxford University Press. Publisher information.

41. Turing, A. M. (1937). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1), 230–265. DOI.

42. Pearl, J. (2009). Causality: Models, reasoning, and inference (2nd ed.). Cambridge University Press. Publisher/DOI.

43. Herdağdelen, A., Joren, H., & Tamkin, A. (2026, October 27). How AI agents shape experts’ judgment calls. Anthropic Research. Experiment report.

44. Hu, S., Huang, L., Deng, Y., & Chen, K. (2026). SciCode-Verified: How benchmark defects underestimated the scientific-coding ability of language models. arXiv. Preprint.

45. Becker, J., Rush, N., Barnes, B., & Rein, D. (2025, July 10). Measuring the impact of early-2025 AI on experienced open-source developer productivity. METR. Randomized study.

46. Becker, J., Rush, N., Cunningham, T., Rein, D., & Mahamud, K. (2026, February 24). We are changing our developer productivity experiment design. METR. Methodological update.

47. Jones, B. F. (2009). The burden of knowledge and the “death of the Renaissance man”: Is innovation getting harder? The Review of Economic Studies, 76(1), 283–317. DOI.

48. Bloom, N., Jones, C. I., Van Reenen, J., & Webb, M. (2020). Are ideas getting harder to find? American Economic Review, 110(4), 1104–1144. DOI.

49. Publication Forum, Mathematics and Statistics Panel. (2026, October 21). Advanced AI and scientific publications: Early evidence from mathematics. Federation of Finnish Learned Societies. Institutional statement.

50. Achim, P. (2026). The verification bottleneck. arXiv. Preprint.

51. Coase, R. H. (1937). The nature of the firm. Economica, 4(16), 386–405. DOI.

52. Mathematics and AI declaration signatories. (2026, September 11). A severe misalignment of AI in mathematics. Math and AI. Community declaration.

53. Advisory Group on Mathematics and Artificial Intelligence. (2026, September 29). Responsible release of AI-generated mathematics. AGMAI. Independent guidance.

54. Simons Foundation. (2026, October 15). Simons Foundation launches $15M effort to help mathematicians navigate AI era. Simons Foundation. Funding announcement.

55. Epoch AI. (2026). FrontierMath: Tiers 1–4 and benchmark methodology. Epoch AI. Benchmark documentation.

56. Wijk, H., Lin, T., Becker, J., Jawhar, S., Parikh, N., Broadley, T., Chan, L., Chen, M., Clymer, J., Dhyani, J., Ericheva, E., Garcia, K., Goodrich, B., Jurkovic, N., Karnofsky, H., Kinniment, M., Lajko, A., Nix, S., Sato, L., … Barnes, E. (2024). RE-Bench: Evaluating frontier AI R&D capabilities of language model agents against human experts. arXiv. Preprint.

57. Starace, G., Jaffe, O., Sherburn, D., Aung, J., Shern, C. J., Maksin, L., Dias, R., Mays, E., Kinsella, B., Thompson, W., Heidecke, J., Glaese, M., Patwardhan, T., & OpenAI. (2025). PaperBench: Evaluating AI’s ability to replicate AI research. OpenAI. Benchmark report.

58. Zhou, J., Sun, Z., Li, B., Zhou, J., Pan, Y., Wang, H., Ren, H., Jia, X., Zhou, X., Cao, X., Chen, Y., Feng, Y., Wu, J., Zhang, C., Chen, S., Xue, H., You, C., Wang, H., Wu, K., … Xie, J. (2026). ASI-Bench: At the dawn of artificial superintelligence. arXiv. Preprint.

59. Epoch AI. (2026, June 12). FrontierMath Tiers 1–3 (v2). Epoch AI. Revised benchmark documentation. The update reports corrections affecting 42% of the original problems.

60. METR. (2026, January 29). Time Horizon 1.1. METR. Evaluation methodology. The task suite grew to 228 tasks, but its authors stress benchmark-composition sensitivity and wide confidence intervals.