Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Auditable AI-Assisted Scientific Discovery: From Noncausal Processes to Quantum Measurement Rigidity

Steven Abel

Published Sep 9, 2026• 0 citations
Publisher

Abstract

Large language models can accelerate scientific exploration, but generated arguments are not evidence. We report a human–AI research workflow in which model outputs are treated as conjectures and claims are admitted only after proof or deterministic, independently checked computation. The workflow is illustrated by a connected sequence of results in mathematical physics. An exhaustive exact search of 19,683 rotation-symmetric ternary process functions finds 111 logically consistent cases, of which 108 are noncausal, and yields a projection-rigidity result over 432 source completions and 5,184 coarse-grainings. These structures generate qutrit product bases. For all 108 noncausal cores, exact orthogonality-preserving measurement calculations certify local rigidity and therefore impossibility of perfect finite-round local-operations-and classical-communication discrimination. An independent exact sweep of all 744 consistent binary tripartite process functions reproduces the qualitative causality/QNLWE boundary implied by recent general theory while additionally certifying local orthogonality-preserving rigidity for all 64 noncausal binary cases. We further obtain a closed-form rigidity spectrum and quantitative finite-round error bounds. Three of four pre-run structural predictions in the first campaign were falsified, and subsequent conjectures were retained when killed. We use this record to distinguish final-answer verification from discovery provenance, contrasting our control-first architecture with the large-scale multi-agent search and Lean verification reported in OpenAI’s September 2026 Navier–Stokes announcement. The general process-function/product-basis correspondence and its qualitative causality/QNLWE equivalence are credited to prior work; the contribution here is the audited research architecture together with the exact ternary census, projection rigidity, stronger local measurement-rigidity certificates, and quantitative results.

DOI
10.6084/m9.figshare.33471943

Related papers

A Human Audit of OpenAIs AI-Generated Mathematical Proofs

Mikołaj Sienicki, Krzysztof Sienicki

We assess 18 chapter-specific reviews of the ten mathematical results announced by OpenAI on 1 August 2026, alongside review standards, Lean formalizations, subsequent research, and mathematical references. The article audits this review record without claiming a complete reconstruction of all ten proofs. No confirmed substantive mathematical error in a principal result remains in the examined assessments, although review depth varies and some dependencies remain partly checked. Chapter 8 presents the strongest reservation: a specialist review requests major revision of compressed analytic arguments. In Chapter 6, an apparent polarity error was withdrawn after an overbar lost during PDF extraction was recovered from the typeset source. Subsequent research independently reuses the Chapter 3 proof mechanism and confirms that Connes's rigidity conjecture is false, without independently reproducing Chapter 4's stronger infinite-family result. Among the cited follow-ups, Chapter 7 receives the strongest direct theorem-level corroboration through a stronger hardness theorem. Related equality results in Chapter 8 do not verify the analytic inequality proof. Some follow-ups disclose material AI assistance. We argue that confidence should combine formal checking, human reconstruction, independent mathematical use, and a public record supporting correction of both proofs and reviews.

cs.AICross-listedarXiv:2608.14673•Aug 4, 2026

From AI-Generated Circuits to Accountable Quantum Execution: A Hybrid Workflow Framework

Taylor Miss

Connecting AI-generated quantum programs to executable experiments requires more than syntactically valid code: the workflow must also control execution authority and preserve the basis for interpreting its results. This paper develops a conceptual architecture organized around three responsibilities: AI-assisted circuit proposal, deterministic classical validation, and quantum measurement execution. A quantum-job contract binds circuit artifacts, measurement settings, resource allocations, backend information, and provenance to explicit admission conditions. The design separates permission to run an experiment from evidence that its output answers the intended scientific question. An analytical single-qubit variational example demonstrates this distinction through exact energy calculations, finite-shot variance, and budget-constrained measurement allocation. Responsibility allocation, runtime interception, and staged transformation provide the architectural principles, while uncertainty reporting and reference calculations supply the scientific checks. A prospective evaluation protocol covers accuracy, policy violations, reproducibility, end-to-end cost, and researcher effort. The framework is presented as a design proposal supported by mathematical illustration, not as a tested implementation; its operational benefits and applicability to larger quantum workloads remain to be established.

•Sep 11, 2026•0 citations

A Consistency Core for Process Matrices, with an Exact Closed-Form Causal Witness for the Oreshkov-Costa-Brukner Process

Rolando P. Hong Enriquez

Process matrices describe correlations with no definite order of operations, and the property that sets a genuinely indefinite process apart from an ordinary mixture of ordered ones is called causal nonseparability. This paper gives a careful, self-contained account of why the whole framework hangs together consistently, across three levels at once, the level of plain probabilities, the level of quantum measurement rules, and the level of classical logical consistency. Its main practical result is an exact, written-out certificate that detects the indefiniteness of the canonical process by hand, replacing a numerical computer search with a formula a reader can check with pencil and paper. Working in a convenient basis in which the relevant bookkeeping operations act especially simply, the paper derives the certificate in closed form as the identity minus two specific order-sensitive terms. It shows that the two natural pieces of this certificate are well-behaved in the technical sense required, each with an explicit, exactly known set of values and an explicit proof of positivity written as a sum of squares. Evaluated on the canonical indefinite process, the certificate returns a specific negative number exactly, which is precisely the signal of indefiniteness. The paper then abstracts the construction into a general recipe, a theorem stating that any certificate of this shape is valid whenever a simple sum-of-squares condition holds on its two pieces. Alongside this it lays out, level by level, how the framework stays consistent, from the requirement that probabilities behave, through the quantum measurement rule, to the classical fixed-point picture in which a would-be paradoxical loop has, or fails to have, a unique consistent resolution. Every numbered result is also formally verified in a machine proof assistant, to the authors' knowledge the first such verification for this framework, with the correspondence to the formal statements collected in an appendix. The value of the paper is to turn what had been the output of an opaque numerical optimizer into a transparent, reusable, and independently machine-checked object that anyone can audit and build on. By exhibiting an exact certificate and a general recipe for producing more, it lowers the barrier to certifying indefinite causal order, and by verifying the whole consistency core in a proof assistant it supplies a dependable formal foundation for later work. The paper is modest about what it adds, presenting the physics of the canonical process as already known and offering instead an exact and verifiable rendering of it.

•Aug 24, 2026•0 citations

Paradox-free classical non-causality and unambiguous non-locality without entanglement are equivalent

Hippolyte Dourdent, Kyrylo Simonov, Andreas Leitherer +5 more

Closed timelike curves (CTCs) challenge our conception of causality by allowing information to loop back into its own past. Any consistent description of such scenarios must avoid time-travel paradoxes while respecting the no-new-physics principle, which requires that the set of operations available within any local spacetime region remain unchanged, irrespective of whether CTCs exist elsewhere. Within an information-theoretic framework, this leads to process functions: deterministic classical communication structures that remain logically consistent under arbitrary local operations, yet can exhibit correlations incompatible with any definite causal order - a phenomenon known as non-causality. In this work, we establish a correspondence between process functions and unambiguous complete product bases, i.e. product bases in which every local state belongs to a unique local basis. This equivalence implies that non-causality of process functions is exactly mirrored by quantum nonlocality without entanglement (QNLWE) - the impossibility of perfectly distinguishing separable states using local operations and causal classical communication - for such bases. Our results generalize previous special cases to arbitrary local dimensions and any number of parties, enable systematic constructions of non-causal process functions and unambiguous QNLWE bases, and implies, inter alia, that bipartite unambiguous QNLWE bases do not exist. Finally, this work reveals an unexpected connection between causal and non-signaling inequalities: every process function both maximally violates an associated causal inequality and yields a corresponding Bell inequality that admits no violation.

quant-pharXiv:2512.23599•Dec 30, 2025•0 citations

Agentic AI for Scientific Reasoning in Autonomous Quantum Sensing Experiments

Takuya Isogawa, Ryotaro Okabe, Nutdech Phadetsuwannukun +2 more

We implement an agentic AI workflow built around a large language model (LLM) agent for autonomous experiments with nitrogen-vacancy (NV) centers in diamond. NV centers are a widely used platform for quantum sensing, and the ability to control many measurements from a computer makes NV experiments a natural setting for autonomous workflows. We make two main contributions. First, we demonstrate an autonomous NV experiment workflow that combines persistent project records, quantitative calculation and data analysis tools, and deterministic experiment control. In one autonomous experiment, the agent selected a single NV center, calibrated its resonant frequency, measured \(T_2^\ast\) with Ramsey measurements, and added a Carr--Purcell--Meiboom--Gill (CPMG) measurement to check a weak feature that could be related to nearby \(^{13}\mathrm{C}\). Second, we introduce two offline benchmarks that evaluate the agent's reasoning separately from laboratory execution. We evaluated both benchmarks with GPT-5.4, GPT-5.5, and GPT-5.6 Sol. In the Ramsey checkpoint benchmark, greater reasoning effort generally improved recognition of a residual resonance calibration offset. By contrast, in the pulsed optically detected magnetic resonance (pODMR) data evaluation benchmark, pulse sequence information alone produced more false positive resonance judgments at higher reasoning effort. Requiring an expected signal calculation kept false positive rates low across all three models and reasoning settings. The results suggest a clear division of labor for autonomous experiments. The agent forms scientific hypotheses and uses quantitative tools to evaluate data, while deterministic code controls the hardware and enforces safety constraints.

quant-pharXiv:2607.25145•Jul 29, 2026•0 citations

Seed IQ's Quantum-Computed Clay Millennium Prize Results, Independently Validated by Frontier Classical AI Labs

Denise Holt, Denis Ovseyenko

Abstract What was computed. In July 2026, AIX Global identified the deciding mathematical objects underlying the six remaining Clay Millennium Prize problems and used Seed IQ governed fault-tolerant quantum computation [2] to compute those objects, with the Poincaré conjecture recovered independently as a positive control. Each computed value was carried into a complete proof of the official Clay statement and machine-checked by the Lean 4 kernel. AIX Global publicly released the six-problem result on 30 August 2026. For Navier–Stokes, the quantum computation established global regularity of the unforced equations by bounding the curvature of the vorticity-direction field wherever the vorticity is intense — the quantity that governs whether vortex stretching can run away. What OpenAI produced. Nine days later, on 8 September 2026, OpenAI announced a finite-time singularity construction for the forced Navier–Stokes equations, produced by approximately 10,000 AI agents over 88 hours of classical computational search. OpenAI did not reach the result AIX Global reached. It did not prove the unforced global-regularity statement, which is the statement the Clay problem poses and the one AIX Global resolved; classical search did not pass that threshold. What its agents produced instead was a construction in which an engineered external force drives the fluid toward singular behavior — the adjacent statement, reachable by search precisely because the singular geometry is supplied rather than derived, and obtained at 88 hours of search and roughly ten million dollars of list-price inference — against 4 h 52 min of metered QPU time and $28,032 for the complete unforced-regularity proof itself [2], and 26.8 QPU-seconds ($42.88) for the six adjudication experiments run against the construction. Because the construction originated outside AIX Global through a radically different computational architecture, it supplied a new external test of the mathematical mechanism underlying the earlier result. What the experiments found. On 13 September 2026, AIX Global again used Seed IQ governed fault-tolerant quantum computation to run six experiments directly against OpenAI’s construction. The external force supplied 97.3% of the measured positive vorticity budget, compared with 2.7% from intrinsic positive stretching. Direction curvature tracked the externally prescribed collapsing scale with correlation 0.81. Preventing that scale from collapsing eliminated the finite-time boundary crossing, while allowing the external feed to decay reduced maximum vorticity from 12.35 to 9.93 and direction curvature from 11.543 to 11.230. No competing intrinsic blow-up mechanism absent from the July computation emerged. The singular trajectory crossed the regularity boundary only when the external forcing supplied and continuously tightened the required geometry, and it relaxed when that forcing decayed. What it establishes. OpenAI’s construction therefore independently and inadvertently validated the central mathematical mechanism of the AIX Global Navier–Stokes result from the opposite direction. The boundary governing the unforced system had already been identified, computed through governed fault-tolerant quantum computation, and carried into a complete proof. OpenAI’s construction did not cross that boundary: its singular behaviour was obtained only because an external force supplied and continuously tightened the geometry the unforced dynamics do not generate — exactly what the AIX Global proof establishes cannot arise on its own. The OpenAI result therefore validates the Navier–Stokes proof attained by AIX Global with Seed IQ. A second independent confirmation appears in the Riemann Hypothesis: on 10 August 2026, before the AIX Global results were public, approximately 60 Anthropic Claude subagents raised the proven proportion of nontrivial zeros on the critical line from 41.6% to 67.2% while leaving the hypothesis itself unresolved, advancing precisely in the direction required by the stronger statement the AIX Global Riemann proof, attained with Seed IQ in July 2026, had already established. The Anthropic result therefore also validates another proof attained by AIX Global with Seed IQ. Neither result reached what Seed IQ produced, and neither closed a proof: OpenAI did not obtain the unforced global-regularity statement, Anthropic did not obtain the Riemann Hypothesis, and in both cases the deciding objects remained out of reach of classical search. Seed IQ identified those objects and governed fault-tolerant quantum computation computed them, which is what allowed both statements to be carried into complete, formally verified proofs.

•Sep 13, 2026•1 citation
Large language models can accelerate scientific exploration, but generated arguments are not evidence. We report a human–AI research workflow in which model outputs are treated as conjectures and claims are admitted only after proof or deterministic, independently checked computation. The workflow is illustrated by a connected sequence of results in mathematical physics. An exhaustive exact search of 19,683 rotation-symmetric ternary process functions finds 111 logically consistent cases, of which 108 are noncausal, and yields a projection-rigidity result over 432 source completions and 5,184 coarse-grainings. These structures generate qutrit product bases. For all 108 noncausal cores, exact orthogonality-preserving measurement calculations certify local rigidity and therefore impossibility of perfect finite-round local-operations-and classical-communication discrimination. An independent exact sweep of all 744 consistent binary tripartite process functions reproduces the qualitative causality/QNLWE boundary implied by recent general theory while additionally certifying local orthogonality-preserving rigidity for all 64 noncausal binary cases. We further obtain a closed-form rigidity spectrum and quantitative finite-round error bounds. Three of four pre-run structural predictions in the first campaign were falsified, and subsequent conjectures were retained when killed. We use this record to distinguish final-answer verification from discovery provenance, contrasting our control-first architecture with the large-scale multi-agent search and Lean verification reported in OpenAI’s September 2026 Navier–Stokes announcement. The general process-function/product-basis correspondence and its qualitative causality/QNLWE equivalence are credited to prior work; the contribution here is the audited research architecture together with the exact ternary census, projection rigidity, stronger local measurement-rigidity certificates, and quantitative results.
We assess 18 chapter-specific reviews of the ten mathematical results announced by OpenAI on 1 August 2026, alongside review standards, Lean formalizations, subsequent research, and mathematical references. The article audits this review record without claiming a complete reconstruction of all ten proofs. No confirmed substantive mathematical error in a principal result remains in the examined assessments, although review depth varies and some dependencies remain partly checked. Chapter 8 presents the strongest reservation: a specialist review requests major revision of compressed analytic arguments. In Chapter 6, an apparent polarity error was withdrawn after an overbar lost during PDF extraction was recovered from the typeset source. Subsequent research independently reuses the Chapter 3 proof mechanism and confirms that Connes's rigidity conjecture is false, without independently reproducing Chapter 4's stronger infinite-family result. Among the cited follow-ups, Chapter 7 receives the strongest direct theorem-level corroboration through a stronger hardness theorem. Related equality results in Chapter 8 do not verify the analytic inequality proof. Some follow-ups disclose material AI assistance. We argue that confidence should combine formal checking, human reconstruction, independent mathematical use, and a public record supporting correction of both proofs and reviews.
Connecting AI-generated quantum programs to executable experiments requires more than syntactically valid code: the workflow must also control execution authority and preserve the basis for interpreting its results. This paper develops a conceptual architecture organized around three responsibilities: AI-assisted circuit proposal, deterministic classical validation, and quantum measurement execution. A quantum-job contract binds circuit artifacts, measurement settings, resource allocations, backend information, and provenance to explicit admission conditions. The design separates permission to run an experiment from evidence that its output answers the intended scientific question. An analytical single-qubit variational example demonstrates this distinction through exact energy calculations, finite-shot variance, and budget-constrained measurement allocation. Responsibility allocation, runtime interception, and staged transformation provide the architectural principles, while uncertainty reporting and reference calculations supply the scientific checks. A prospective evaluation protocol covers accuracy, policy violations, reproducibility, end-to-end cost, and researcher effort. The framework is presented as a design proposal supported by mathematical illustration, not as a tested implementation; its operational benefits and applicability to larger quantum workloads remain to be established.
Process matrices describe correlations with no definite order of operations, and the property that sets a genuinely indefinite process apart from an ordinary mixture of ordered ones is called causal nonseparability. This paper gives a careful, self-contained account of why the whole framework hangs together consistently, across three levels at once, the level of plain probabilities, the level of quantum measurement rules, and the level of classical logical consistency. Its main practical result is an exact, written-out certificate that detects the indefiniteness of the canonical process by hand, replacing a numerical computer search with a formula a reader can check with pencil and paper. Working in a convenient basis in which the relevant bookkeeping operations act especially simply, the paper derives the certificate in closed form as the identity minus two specific order-sensitive terms. It shows that the two natural pieces of this certificate are well-behaved in the technical sense required, each with an explicit, exactly known set of values and an explicit proof of positivity written as a sum of squares. Evaluated on the canonical indefinite process, the certificate returns a specific negative number exactly, which is precisely the signal of indefiniteness. The paper then abstracts the construction into a general recipe, a theorem stating that any certificate of this shape is valid whenever a simple sum-of-squares condition holds on its two pieces. Alongside this it lays out, level by level, how the framework stays consistent, from the requirement that probabilities behave, through the quantum measurement rule, to the classical fixed-point picture in which a would-be paradoxical loop has, or fails to have, a unique consistent resolution. Every numbered result is also formally verified in a machine proof assistant, to the authors' knowledge the first such verification for this framework, with the correspondence to the formal statements collected in an appendix. The value of the paper is to turn what had been the output of an opaque numerical optimizer into a transparent, reusable, and independently machine-checked object that anyone can audit and build on. By exhibiting an exact certificate and a general recipe for producing more, it lowers the barrier to certifying indefinite causal order, and by verifying the whole consistency core in a proof assistant it supplies a dependable formal foundation for later work. The paper is modest about what it adds, presenting the physics of the canonical process as already known and offering instead an exact and verifiable rendering of it.
Closed timelike curves (CTCs) challenge our conception of causality by allowing information to loop back into its own past. Any consistent description of such scenarios must avoid time-travel paradoxes while respecting the no-new-physics principle, which requires that the set of operations available within any local spacetime region remain unchanged, irrespective of whether CTCs exist elsewhere. Within an information-theoretic framework, this leads to process functions: deterministic classical communication structures that remain logically consistent under arbitrary local operations, yet can exhibit correlations incompatible with any definite causal order - a phenomenon known as non-causality. In this work, we establish a correspondence between process functions and unambiguous complete product bases, i.e. product bases in which every local state belongs to a unique local basis. This equivalence implies that non-causality of process functions is exactly mirrored by quantum nonlocality without entanglement (QNLWE) - the impossibility of perfectly distinguishing separable states using local operations and causal classical communication - for such bases. Our results generalize previous special cases to arbitrary local dimensions and any number of parties, enable systematic constructions of non-causal process functions and unambiguous QNLWE bases, and implies, inter alia, that bipartite unambiguous QNLWE bases do not exist. Finally, this work reveals an unexpected connection between causal and non-signaling inequalities: every process function both maximally violates an associated causal inequality and yields a corresponding Bell inequality that admits no violation.
We implement an agentic AI workflow built around a large language model (LLM) agent for autonomous experiments with nitrogen-vacancy (NV) centers in diamond. NV centers are a widely used platform for quantum sensing, and the ability to control many measurements from a computer makes NV experiments a natural setting for autonomous workflows. We make two main contributions. First, we demonstrate an autonomous NV experiment workflow that combines persistent project records, quantitative calculation and data analysis tools, and deterministic experiment control. In one autonomous experiment, the agent selected a single NV center, calibrated its resonant frequency, measured T2∗T_2^\astT2∗​ with Ramsey measurements, and added a Carr--Purcell--Meiboom--Gill (CPMG) measurement to check a weak feature that could be related to nearby 13C^{13}\mathrm{C}13C. Second, we introduce two offline benchmarks that evaluate the agent's reasoning separately from laboratory execution. We evaluated both benchmarks with GPT-5.4, GPT-5.5, and GPT-5.6 Sol. In the Ramsey checkpoint benchmark, greater reasoning effort generally improved recognition of a residual resonance calibration offset. By contrast, in the pulsed optically detected magnetic resonance (pODMR) data evaluation benchmark, pulse sequence information alone produced more false positive resonance judgments at higher reasoning effort. Requiring an expected signal calculation kept false positive rates low across all three models and reasoning settings. The results suggest a clear division of labor for autonomous experiments. The agent forms scientific hypotheses and uses quantitative tools to evaluate data, while deterministic code controls the hardware and enforces safety constraints.
Abstract What was computed. In July 2026, AIX Global identified the deciding mathematical objects underlying the six remaining Clay Millennium Prize problems and used Seed IQ governed fault-tolerant quantum computation [2] to compute those objects, with the Poincaré conjecture recovered independently as a positive control. Each computed value was carried into a complete proof of the official Clay statement and machine-checked by the Lean 4 kernel. AIX Global publicly released the six-problem result on 30 August 2026. For Navier–Stokes, the quantum computation established global regularity of the unforced equations by bounding the curvature of the vorticity-direction field wherever the vorticity is intense — the quantity that governs whether vortex stretching can run away. What OpenAI produced. Nine days later, on 8 September 2026, OpenAI announced a finite-time singularity construction for the forced Navier–Stokes equations, produced by approximately 10,000 AI agents over 88 hours of classical computational search. OpenAI did not reach the result AIX Global reached. It did not prove the unforced global-regularity statement, which is the statement the Clay problem poses and the one AIX Global resolved; classical search did not pass that threshold. What its agents produced instead was a construction in which an engineered external force drives the fluid toward singular behavior — the adjacent statement, reachable by search precisely because the singular geometry is supplied rather than derived, and obtained at 88 hours of search and roughly ten million dollars of list-price inference — against 4 h 52 min of metered QPU time and $28,032 for the complete unforced-regularity proof itself [2], and 26.8 QPU-seconds ($42.88) for the six adjudication experiments run against the construction. Because the construction originated outside AIX Global through a radically different computational architecture, it supplied a new external test of the mathematical mechanism underlying the earlier result. What the experiments found. On 13 September 2026, AIX Global again used Seed IQ governed fault-tolerant quantum computation to run six experiments directly against OpenAI’s construction. The external force supplied 97.3% of the measured positive vorticity budget, compared with 2.7% from intrinsic positive stretching. Direction curvature tracked the externally prescribed collapsing scale with correlation 0.81. Preventing that scale from collapsing eliminated the finite-time boundary crossing, while allowing the external feed to decay reduced maximum vorticity from 12.35 to 9.93 and direction curvature from 11.543 to 11.230. No competing intrinsic blow-up mechanism absent from the July computation emerged. The singular trajectory crossed the regularity boundary only when the external forcing supplied and continuously tightened the required geometry, and it relaxed when that forcing decayed. What it establishes. OpenAI’s construction therefore independently and inadvertently validated the central mathematical mechanism of the AIX Global Navier–Stokes result from the opposite direction. The boundary governing the unforced system had already been identified, computed through governed fault-tolerant quantum computation, and carried into a complete proof. OpenAI’s construction did not cross that boundary: its singular behaviour was obtained only because an external force supplied and continuously tightened the geometry the unforced dynamics do not generate — exactly what the AIX Global proof establishes cannot arise on its own. The OpenAI result therefore validates the Navier–Stokes proof attained by AIX Global with Seed IQ. A second independent confirmation appears in the Riemann Hypothesis: on 10 August 2026, before the AIX Global results were public, approximately 60 Anthropic Claude subagents raised the proven proportion of nontrivial zeros on the critical line from 41.6% to 67.2% while leaving the hypothesis itself unresolved, advancing precisely in the direction required by the stronger statement the AIX Global Riemann proof, attained with Seed IQ in July 2026, had already established. The Anthropic result therefore also validates another proof attained by AIX Global with Seed IQ. Neither result reached what Seed IQ produced, and neither closed a proof: OpenAI did not obtain the unforced global-regularity statement, Anthropic did not obtain the Riemann Hypothesis, and in both cases the deciding objects remained out of reach of classical search. Seed IQ identified those objects and governed fault-tolerant quantum computation computed them, which is what allowed both statements to be carried into complete, formally verified proofs.