LLM-Aided Proof of an 18-Year-Old Quantum Query Complexity Conjecture, with Formal Verification as the Key

1. The Event: An 18-Year-Old Problem “Solved in Days”

According to reports, a conjecture in quantum computing theory that had remained open since around 2008, and had carried a long-standing bounty, was proved within days by a research system using large language model (LLM) capabilities that were not publicly available at the time. The proof was then fully checked by a formal verification tool.

The important point is not simply that “AI is fast,” but the reliability structure of the workflow: a candidate proof is generated by an LLM, but the final conclusion is not accepted based on the model’s assurance. Instead, it is checked step by step by an independent mechanical verification kernel. This produces a proof certificate that can be reviewed, reproduced, and independently verified by others, rather than a text that merely looks plausible.

2. What Was the Conjecture? The Boundary of Quantum Query Complexity

To explain the conjecture in accessible terms, it helps to start with the concept of query complexity: an algorithm solves a problem by repeatedly accessing the input data, or “querying” an oracle, and the efficiency metric is how many queries are made.

Under this model, a long-standing core question is: how much speedup can quantum algorithms obtain compared with classical randomized algorithms?

• Classical algorithms typically need about N queries for unstructured search, while quantum algorithms, such as those based on amplitude amplification, need only about √N queries, giving a quadratic speedup.
• A sharper question is whether, for arbitrary Boolean functions—especially promise problems—quantum query complexity can be superpolynomially separated from classical randomized query complexity.

The conjecture can be roughly stated as follows: quantum query complexity and classical randomized query complexity differ by at most a polynomial factor, approximately a quadratic factor. If true, this would mean that in the query model for Boolean functions, quantum computing cannot provide an exponential advantage.

3. Why Can LLMs Take Part in Mathematics?

Traditionally, progress on this kind of problem depends on long-term accumulation by a small number of experts. LLMs can change the pace because they automate several parallelizable parts of mathematical research:

1. Candidate strategy generation: Based on large amounts of formal mathematical corpora, a model can quickly generate multiple proof ideas, lemma decompositions, and substitution plans.
2. Lemma filling and rewriting: For intermediate steps, the model can generate auxiliary lemmas, equivalent transformations, or inductive assumptions, reducing the chance of getting stuck at a single step.
3. Autoformalization: Natural-language statements and reasoning can be translated into strict statements that can be mechanically checked by a proof assistant.
4. Very low trial-and-error cost: Rejecting a candidate proof is far cheaper than the time a human would spend pursuing an incorrect direction.

In other words, LLMs do not “guarantee correctness.” Instead, they place high-value candidates in front of the verifier at an unprecedented speed.

4. Formal Verification: Why AI Proofs Must Pass a “Machine Security Check”

This is the most easily overlooked but most critical part of the event.

LLMs can hallucinate: they may produce reasoning that reads rigorously but is actually flawed. The value of formal verification is that it blocks this “seemingly correct but incorrect” risk:

• Trusted kernel: A proof assistant is based on foundations such as type theory. A proof is accepted only if it is checked step by step by the kernel; everything outside the kernel, including AI-generated strategies, is treated as untrusted input.
• Reproducible certificate: A verified proof is a deterministic, machine-replayable artifact. Anyone can rerun it and obtain the same conclusion.
• Failure as feedback: When a proof fails, the verifier points out unresolved subgoals or type errors. This structured feedback can be fed back to the model to drive the next round of generation.

Therefore, “AI + formal verification” is a typical neuro-symbolic collaboration: the model handles imagination and search, while the kernel guarantees correctness. This division of labor allows high-speed generation without sacrificing the reliability of the conclusion.

5. What This Means for Quantum Computing: Where Exponential Speedup Comes From

If the conjecture is indeed true, as indicated by the verified proof, its significance is that it defines the boundary of quantum speedup:

• For general Boolean function problems, quantum computing is likely to provide only polynomial speedup, not exponential speedup.
• Quantum algorithms with true exponential advantages, such as those based on period finding or hidden subgroup structure, do not gain their power from generic “computational superiority.” Instead, their speedup comes from special algebraic structure in the problem itself.
• This turns the question of when quantum computing can exponentially outperform classical computing from a vague slogan into a definable technical condition: the answer depends on problem structure, not on a generic claim that “quantum is faster.”

For engineering and research, this is a valuable criterion: when designing quantum algorithms, one should prioritize problems with exploitable algebraic structure rather than expecting universal acceleration.

6. Engineering Perspective: Building an “AI Generation + Machine Verification” Research Loop

If this paradigm is to be reused in practical development, the process can be abstracted into the following loop. The code below is illustrative pseudocode and does not represent any specific product interface.

# Illustrative pseudocode: AI generation + machine verification loop
def solve_with_formal_loop(conjecture_nl):
    stmt = autoformalize(conjecture_nl)          # natural language -> formal statement
    library = load_verified_corpus()             # verified lemma library used as context
    feedback = []
    for round in range(max_rounds):
        candidates = llm.propose_proofs(stmt, context=library)
        for cand in candidates:
            ok, residual_goals = verifier.check(cand)   # independent kernel checks proof mechanically
            if ok:
                return certify(cand)                    # passed => trusted certificate
            feedback.append(residual_goals)             # failed goals are fed back
        stmt = llm.refine(stmt, feedback)               # refine strategy based on feedback
    raise ProofNotFound

Around this loop, engineering efforts should focus on several areas:

• Context engineering: Providing a verified theorem library and relevant lemmas as retrieval-augmented context can significantly improve candidate quality.
• Reproducibility: Fix random seeds, record model versions and verifier versions, and ensure results can be replayed.
• Compute and storage coordination: Large-scale candidate generation is compute-intensive. Elastic container platforms, object storage, and message queues can be used to schedule tasks and retain intermediate artifacts. Logging and monitoring can track verification pass rates, failure modes, and costs.
• Failure-mode analysis: Clustering the types of errors most often rejected by the verifier can provide direct input for improving prompts and retrieval strategies.

7. Rational Assessment: Limitations, Risks, and Misconceptions

• Do not overstate generality: Proving one conjecture does not mean AI can universally replace mathematicians. Many open problems lack a clear formalizable structure.
• Trust the verified proof, not the model’s assertion: Without formal verification, AI-generated proofs should be treated with caution.
• Formalization itself is difficult: Strictly formalizing a conjecture remains a major challenge. Incorrect modeling may make a proof technically valid in literal form while deviating from the original intent.
• Compute cost is significant: Large-scale proof search is resource-intensive and requires reasonable scheduling and budget control.
• Human-AI division of labor: A more realistic picture is a three-way collaboration: AI accelerates search, humans choose problems and handle modeling, and machines ensure correctness.

8. Conclusion and Implications

The real signal of this event is not that a particular model “became a little stronger,” but that the research paradigm combining AI with formal verification is maturing. LLMs dramatically reduce the search cost in mathematics and theoretical computer science, while formal verification provides a correctness guarantee.

For quantum computing, this also turns the broad question of whether quantum computers can exponentially outperform classical computers into a definable and verifiable technical condition.

For developers and researchers, the implication is straightforward: instead of waiting for a “general artificial intelligence miracle,” it is better to build a reproducible “generate–verify–feedback” loop now, constraining AI capabilities to a track that can be mechanically checked, so that acceleration can be translated into trustworthy results.