AI Solved an 18-Year-Old Quantum Query Complexity Conjecture in Three Days: What It Actually Means

1. Facts First, Rumors Later

According to publicly disclosed information, the sequence of events was roughly this: a research system at a certain institution — reported to run on a large model more capable than, and not publicly released as, the available versions — produced a proof of a quantum query complexity conjecture that had remained open since 2008 on the third day of the task. That proof was then checked in full by an interactive theorem prover.

Two layers here have to be kept separate.

The first is the rumor layer about “model capability”: parameter counts, internal versions, training recipes. None of it comes with verifiable public evidence, and from an engineering standpoint it should simply be ignored. The second is the verifiable output: a proof that a machine can check line by line and that anyone can re-run. That is the signal that actually carries value, because it turns an unreproducible verbal claim into an auditable technical artifact.

The correct order for judging the credibility of news like this is: find the formalized statement first, then the proof script, then the checking command and version numbers, and only at the end look at the narrative. Running that order in reverse makes it very easy to get swept along by “the future is already here” rhetoric.

2. What the Conjecture Asks: Why Quantum Speedups “Need Structure”

The conjecture comes from the query complexity (oracle) model. This model does not assume the algorithm knows the concrete encoding of its input; it can only access data by “querying the i-th input bit” one at a time, and it counts the number of queries rather than the size of the gate circuit. The advantage is that clean lower bounds can be proven at the information-theoretic level, and that the classical deterministic, classical randomized, and quantum query models line up in a well-defined one-to-one correspondence.

The conjecture that fell is the best known statement in this family. Its core question is whether, for a “partial Boolean function” defined on some subset of the input space, the quantum query complexity is polynomially bounded from above by some classical sensitivity-type measure, with the bound being quadratic in degree.

Why was this worth an 18-year bounty? Because it touches a foundational question in quantum computing theory: where does exponential quantum speedup actually come from.

The consensus understanding that has formed is that in the purest “structureless” setting, the quantum advantage over classical algorithms is limited. For functions over point sets accessed by queries, quantum algorithms typically achieve only a quadratic speedup, the same order of magnitude as Grover-style search. The cases that open up a genuinely exponential gap almost all rely on some additional structure: periodicity (such as the hidden subgroup structure underlying discrete logarithm and integer factorization), permutations over a symmetry group, or a strong promise on the input. A partial function is precisely the kind of object that is “only responsible for part of its inputs,” so it naturally carries promise information.

The real question these conjectures pose is therefore whether the growth of classical measures is already “locked” within some polynomial range of quantum query complexity. If the answer is yes, then no free extra speedup can be collected on partial functions via the promise, and the source of quantum advantage is pinned down in a much clearer place. If the answer is no, then a batch of previously unidentified speedup examples exists. Whichever way it lands, it directly reshapes how research effort in the field is allocated for the following decade.

3. What “Finished on Day Three” Means: The Model Is One Component of a Search Engine

One common misreading needs correcting: the large model did not “figure it out by itself.” It worked as a policy component inside a proof search system. The mainstream “AI plus formal verification” paradigm can be decomposed into four independently replaceable parts.

The formalized statement. Translating a natural-language proposition into a formal statement expressible in the proof assistant’s type system, including every quantifier, domain constraint, and constant value. The error rate at this stage is often higher than in the proof itself, and an error here will not be caught automatically.

The policy model. It receives the current proof state (goal, contextual assumptions, available lemmas) and outputs the next tactic or theorem-application suggestion. Its job is to compress the branching factor of the search tree, not to guarantee correctness.

Sampling and parallelism. The same state can be expanded in parallel into tens of thousands of candidate paths, and with best-first-style search scheduling this routes around the local dead ends that depth-first search tends to fall into.

The checker. Every candidate proof must ultimately be validated rule by rule by the kernel, and anything that fails is discarded. This is the only component in the whole system that holds veto power.

So what “solved in three days” really means is usually this: across hundreds to thousands of GPU hours of parallel sampling, policy model plus lemma reordering plus search scheduling happened to hit the correct path. Day three is the result of a scheduling and sampling budget, not the moment when “comprehension suddenly clicked.”

# Illustrative orchestration logic; not any vendor's real interface
def search_proof(goal, budget):
    queue = PriorityQueue(root_state(goal))
    visited = set()
    while queue and budget.remaining() > 0:
        state = queue.pop()
        if verifier.is_closed(state):
            return state.proof            # the only success criterion
        key = canonical(state)
        if key in visited:
            continue
        visited.add(key)
        for step in policy.sample(state, k=beam_width, temperature=1.0):
            nxt = step.apply(state)
            if verifier.admissible(nxt):  # fast pruning: type-legal, goal makes progress
                queue.push(nxt, score=heuristic(nxt))
    return None

Three design points in this code are worth noting: there is exactly one success criterion, the kernel check; the heuristic affects efficiency only, never correctness; and the visited set must be keyed on a canonical representation of the state, otherwise the same goal re-enters the queue in countless equivalent forms and much of the sampling budget is wasted.

4. What a Machine-Checked Proof Actually Buys You: Verifiable and Reproducible, Not Necessarily Understandable

What formal verification provides for this proof is “relative certainty,” not absolute truth.

The part it settles includes: every inference step conforms to the rules of the underlying type theory; there are no skipped steps, no “obviously follows,” no references to lemmas that do not exist; and anyone holding the same version of the proof script and the same pinned dependency versions will reach the same “pass” conclusion. Compared with traditional mathematics, where peer review checks a paper段落 by段落, this is a genuine order-of-magnitude improvement in reliability, especially when the proof runs to hundreds of pages.

The part it does not settle is equally clear:

• Faithfulness of the statement. If the formalization carelessly simplified a quantifier’s range, a domain, or a constant’s value, the machine will faithfully verify a weaker proposition. This “verified, but not the original problem” failure is the most dangerous class of error in formalization work.
• Trustworthiness of the dependency library. A proof typically builds on a foundational mathematics library whose correctness forms the trust root. Any tool can have implementation defects, which is why industrial-strength processes lock versions and audit dependencies rather than pulling the latest branch at will.
• Human comprehensibility. A machine-checked proof may be tens of thousands of lines of unstructured combinatorial search output. It answers “does it hold,” not “why it holds,” which makes it hard to transfer directly to neighboring propositions. This is also why research systems usually ship a condensed human-readable version alongside.

For engineering teams there is one transferable lesson here: the value of any AI-generated artifact depends on whether a cheap, automatic verification stage exists downstream that the generating party cannot manipulate. A theorem prover happens to be an ideal verifier of this kind — far cheaper than generation, and fully decoupled from the thing being verified.

5. Putting It Into Practice: Building an AI Plus Formal Proof Pipeline

To apply this paradigm to your own work, design it in the following layers.

Task decomposition and budget control. Have humans supply the top-level theorem tree first, split the large proposition into lemmas, then allocate an independent sampling budget to each lemma. The practical rule of thumb is to reserve three to five times the normal budget for “critical lemmas,” and to downgrade automatically to “report partial progress” when a budget is exhausted, so that a single dead end cannot consume the entire batch.

Statement formalization and regression testing. This is where human effort pays off most. The recommended approach is to give each formalized statement a set of “negative cases”: deliberately wrong variants (a quantifier direction reversed, a domain widened, a constant missing a factor) that should be unprovable in the checker. Only when every negative case is correctly rejected can you consider the statement an adequate rendering of the original.

# Illustrative negative-case regression for a formalized statement
CASES = [
    (aa_conjecture_correct,   expect=PROVABLE),
    (aa_domain_widened,       expect=UNPROVABLE),
    (aa_constant_weakened,    expect=UNPROVABLE),
    (aa_quantifier_flipped,   expect=UNPROVABLE),
]
assert all(verifier.provable(c.stmt) == c.expect for c in CASES)

Reproducible experiments and infrastructure. Search-based experiments are extremely sensitive to randomness, so random seeds, policy model version, pinned dependency versions, and search scheduling parameters must all be written into the artifact manifest. On the infrastructure side, you can compose several generic capabilities as needed: a container platform to run elastic GPU jobs and parallelize at lemma granularity; object storage to archive proof scripts, search traces, and checker logs so everything remains traceable; a message queue to distribute lemma-level subtasks and retry failures; and a logging service with alerting to track key metrics — average samples per lemma, kernel check timeout rate, share of statements rejected. These metrics usually tell you more about pipeline health than “how many cards we burned in total.”

One often-overlooked point in metric design: candidates that time out in the checker should not be discarded as failures, but tracked separately. A timeout usually means the proof idea is right but the proof is too long, which makes it a good candidate for a second pass with a “compression policy.”

6. Which Business Scenarios Fit This Paradigm

Formal verification applies to a narrower surface than people assume, but the payoff inside that surface is very high. The test is whether the proposition can be written as a formal statement independent of the runtime environment, and whether the cost of an error is high enough to justify the formalization cost.

Typical high-value scenarios include security properties of cryptographic protocols (formal reductions for non-repudiation or key indistinguishability, for example); invariants and safety properties of consensus and distributed protocols (liveness, linearizability, absence of forks); semantic preservation in compiler optimizations; memory safety on critical paths in kernels or drivers; and machine checking of rule consistency in finance and compliance.

Conversely, scenarios that depend on large amounts of implicit domain knowledge, whose input space cannot be enumerated, or whose notion of correctness rests on human taste and experience (UI interaction quality, the readability of business rules, the soundness of a code architecture) should not be forced into formal verification. The cost will far exceed the benefit.

7. Five Misreadings to Avoid

1. Treating “three days” as a capability benchmark. A single data point is heavily influenced by luck, budget, and problem selection, and constitutes no measure of capability. To assess capability, run repeated sampling on the same lemma set and report the distribution of solve rates rather than the best result.
2. Extrapolating the theorem into engineering performance. Query complexity describes a relative number of queries and cannot be converted directly into wall-clock time or cost advantage on any real hardware.
3. Reading “exponential speedup” as already engineered. A theoretical result only delimits the boundary of what is possible; a considerable distance usually remains between the proposition and a usable algorithm.
4. Underestimating formalization cost. In practice, the human effort spent formalizing statements often exceeds the effort spent on proof search, and lowballing that portion is the most common reason these projects fail.
5. Skipping human review. Even after a machine check passes, someone familiar with the domain should read the condensed proof, focusing on whether the statement is faithful to the original proposition.

8. Conclusion

What is genuinely worth attention here is not what some model finished on the third day, but that it validated an engineering path: in domains where “the proposition can be formalized and the verifier is cheap enough,” generation and verification can be decoupled, freeing researchers from mechanical deduction work so they can focus on posing questions and designing strategies.

For engineering teams, three transferable conclusions follow. Any AI-generated artifact should come with an automatic verifier far cheaper than the generation itself. The correctness of a formalized statement requires independent testing and cannot be assumed. Reproducibility of search-based experiments depends on complete records of randomness, versions, and scheduling parameters. None of the three has anything to do with quantum computing — they apply to almost any setting where AI is brought into a core R&D workflow.