1. First, Treat This Disclosure as an “Unverified Case”

The claim under discussion is that an AI system helped make progress on a quantum complexity conjecture that has been open since 2008, producing a key proof path in a short time and passing validation with formal verification tools.

As of the time of writing, I have not obtained verifiable primary materials: no conjecture name, no research team, no model name, no proof language, no verifier version, no preprint identifier, and no official announcement link.

Therefore, this article treats the claim as an anonymous case and does not endorse its truthfulness. Before citing or forwarding such a claim, you should at least verify the following five items:

1. The original preprint or formal paper, including arXiv identifier, DOI, and publication status.
2. The conjecture name and the original literature proposing it, confirming whether it is the “main conjecture” or only “a lemma / special case.”
3. The model and system names, versions, and whether prompts and retrieval libraries were disclosed.
4. The formal verification repository, proof language, theorem library version, and commit.
5. Whether independent researchers in the field have reproduced the result or issued peer-review comments.

Until these items are available, the correct description is “assisted proof exploration” or “generating candidate proof paths,” not “cracked” or “solved.”

2. Why Quantum Complexity Conjectures Are Hard: First Define the Model Boundary

Quantum computing attracts attention because it may offer significant speedups over classical computation for specific tasks, such as large integer factorization, quantum system simulation, certain sampling tasks, and some linear-algebra tasks.

However, “a quantum algorithm can solve a problem” is not the same as “quantum computing completely outperforms classical computing in engineering practice.” Between these two statements lies the model definition.

Before discussing complexity, you must specify the model; otherwise, conclusions are not comparable:

Model	Resource Measured	What the Conclusion Can Support
Classical deterministic / randomized computation (P, BPP)	Time, space	Cost lower bounds executable on real CPUs/GPUs
Quantum query model (BQP-query, lower hierarchies)	Number of black-box interactions	Constrains query count only; not equal to real circuit cost
Quantum circuit model	Gate count, circuit depth, qubit count	Theoretical implementability; still requires error-correction overhead
Noisy / near-term device model (NISQ)	Noise rate, fidelity, observable circuit depth	Whether something can actually run in practice

Therefore, solving a single conjecture usually resolves only one local problem in the complexity landscape: proving a quantum query lower bound for some function class, establishing an inclusion or separation between quantum and classical complexity, or ruling out a possible separation.

Such a result can redraw the boundary of quantum advantage, but it does not prove that “universal quantum computing has comprehensively surpassed classical computing.” The value of this class of result is mainly theoretical clarification: it tells researchers which advantages are structurally possible and which routes can be abandoned.

3. Turning Proof Search into an Engineering Problem: A Six-Step Closed Loop

A complex conjecture’s proof is rarely a single path. It requires selecting appropriate intermediate lemmas, constructing functions, choosing inequality directions, or identifying counterexample boundaries.

The abstract closed loop can be described as follows:

1. Problem formalization: convert a natural-language conjecture into formal definitions, assumptions, target statements, and a resource model.
2. Knowledge retrieval: recall reusable structures from theorem libraries, papers, and existing formalized code.
3. Candidate generation: the model proposes lemmas, constructions, and counterexample templates.
4. Proof construction: expand candidate ideas into complete derivations.
5. Mechanical verification: the verifier checks each step.
6. Failure attribution: locate erroneous steps, missing assumptions, or invalid references, then refine the problem and search again.

Illustrative Pseudocode (Not a Production Implementation)

The following code is only meant to illustrate the process shape. It is not a runnable system. A real implementation would still need dependencies, budgets, and stopping conditions.

# Dependencies (illustrative; pin actual versions)
# - Proof language: Lean 4 / Rocq (Coq) / Isabelle-HOL
# - Theorem library: Mathlib (fixed tag + commit) or a standard-library snapshot
# - Retrieval: vector database + structured theorem index + permission filtering
# - Orchestration: task queue + containerized verification sandbox
problem = formalize(conjecture)          # Output: definitions, target statement, assumptions
# Resource budget (must be explicit; otherwise the search cannot terminate)
budget = {
    "wall_clock": 72h,
    "llm_tokens": 5e8,
    "verifier_calls": 200000,
    "max_proof_depth": 40
}
while not solved and budget.remaining() > 0:
    context = retrieve_knowledge(problem, top_k=50, filter=policy)
    ideas = model.propose_lemmas(problem, context, temperature=0.8)
    ideas = rank(ideas, key=[novelty, relevance, verifier_cost])
    for idea in ideas:
        proof = model.construct_proof(idea, max_depth=budget.max_proof_depth)
        if proof.has_sorry() or proof.uses_forbidden_axioms():
            log(skip=proof, reason="axiom_or_sorry"); continue
        if verifier.check(proof) == PASS:
            return verified_proof(proof, trace=full_trace())
        feedback = verifier.diagnose(proof)   # error location + missing lemmas + type mismatch points
        problem = refine(problem, feedback)  # add assumptions / change goal / split lemmas
return status(UNSOLVED, evidence=leaderboard_of_best_attempts)

Stopping conditions (if any one is missing, costs will burn out): budget exhaustion, verifier making no new progress for N consecutive rounds, the feasible lemma graph becoming empty, or an expert determining that the current formalization is wrong.

Required log fields: problem ID, hash of the original conjecture and formalized statement, model name and prompt version, retrieval evidence IDs and library snapshot, proof-path ID, verifier version, theorem library version and commit, verification result and first error coordinate, manual revision records, timestamps, and token/compute consumption.

Verification failure categories (this is the most valuable asset):

• STEP_ERROR: invalid single-step reasoning.
• TYPE_MISMATCH: type or definition mismatch; most likely a formalization error.
• MISSING_LEMMA: a known or unproven lemma is missing.
• INSUFFICIENT_HYPOTHESIS: assumptions are insufficient; the original conjecture has been written too weakly.
• GOAL_MISSTATED: the proof establishes another statement rather than the intended one (semantic misalignment; the most dangerous case).
• RESOURCE_EXCEEDED: timeout or budget exceeded; not a logical error.
• RETRIEVAL_MISS: a usable result existed in the library but was not retrieved.

4. Formal Verification: Details Decide Whether It Is a Defense or a Rubber Stamp

The biggest risk of AI-generated proofs is the “pseudo-proof”: fluent text and seemingly complete steps, but with hidden circular reasoning, out-of-scope assumptions, or semantic misalignment.

Formal verification breaks a proof into machine-checkable derivations. However, “verification passed” requires four prerequisites to be meaningful:

1. Proof language and kernel: Lean 4, Rocq/Coq, and Isabelle/HOL have different trusted kernels. You must state which one is used and whether extra axioms are trusted (for example, Classical.choice and propext should be listed).
2. Theorem library version and commit: Mathlib changes constantly. A claim of “already formalized” without a version number is not reproducible. Reviewers should fix the tag and commit, and check for sorry, admit, and unproven environmental assumptions.
3. Verifier interface: the model side and verifier side interact through LSP / JSON-RPC / tactic protocols. The interface must return precise error coordinates (file, line, column, expected type, actual type); otherwise the feedback loop cannot close.
4. Human review nodes (cannot be skipped): definition review → lemma list review → semantic alignment review between the final statement and the original conjecture → authorship and responsibility confirmation.

Typical failure examples: an AI-generated “proof” may compile, but:

(a) it rewrites ∀ε>0, ∃N as ∃N, ∀ε>0;
(b) it introduces stronger assumptions to make the proof go through;
(c) it ends with exact h', where h' is an unproven lemma marked as sorry;
(d) it proves the converse or only a special case, not the main conjecture.

All four must be blocked by human review and automated checks such as sorry scanning, axiom scanning, and item-by-item comparison against the original literature.

Conclusion: formal verification is a trust-enhancing layer, not an automatic correctness certificate. It guarantees that “the derivation is legal,” but it does not guarantee that “the statement is correct.”

5. Quantum Advantage Is Not Universal Superiority: A Five-Item Checklist

To judge whether “quantum advantage” holds, check the following items. If any item fails, you cannot claim an advantage:

Check	Question to Ask	Common Misjudgment
Problem structure fit	Does it rely on specific structures such as period finding or quantum-state simulation?	Generalizing a special-case result to all optimization problems
Resource model clarity	Are you comparing query complexity or real circuit depth, gate count, and measurement count?	Comparing query count with classical algorithm runtime
Noise and error correction	Is the required fault-tolerance overhead achievable on foreseeable hardware?	Ignoring error correction, which can reduce effective gate count by several orders of magnitude
Classical algorithm progress	Has the advantage already been compressed by better classical algorithms or tensor-network methods?	Using a ten-year-old classical baseline for comparison
Engineering reusability	Can it become a compiler, library, or cloud service, rather than a one-off experiment?	Treating a paper result as a sellable product capability

Therefore, a theoretical breakthrough is better understood as a “theory map update,” not an “industrial capability jump.”

For enterprises, the short-term focus should be on engineering scenarios: quantum chemistry and molecular simulation, optimization modeling, sampling-based validation, and cryptographic impact assessment, including post-quantum migration timelines.

6. How Enterprises Should Build Research Agents: Selection, Implementation, and Common Mistakes

1. Scenario Selection Evaluation Table (All Five Must Pass Before Launch)

Dimension	Acceptance Criterion	Failure Sign
Objective decidability	Success or failure has a clear decision function	Only vague goals such as “better quality”
Step verifiability	Intermediate outputs can be automatically checked	Intermediate results can only be judged by humans reading text
Error feedback	Errors can be localized to specific steps	Only a single overall score is provided
Permission control	Knowledge and data can be isolated by role	Full library is open to everyone
Compliance and auditability	Inputs, models, evidence, and conclusions are traceable throughout	Results cannot be traced to sources

Suitable starting scenarios: formalized mathematics, code correctness verification, complex rule reasoning, molecular property prediction with structured constraints, and industrial simulation parameter optimization.

Common mistake: choosing an “open-ended research topic” first, without a decision function. In that case, the system can only rely on human evaluation and cannot close the loop.

2. Knowledge Governance: Manage with Metrics, Not Feelings

A unified knowledge layer should include papers and abstracts, theorem libraries, experimental data, internal specifications, review records, and a failure-case library.

Retrieval should combine keywords + semantics + structured filtering + permissions.

Key metrics: citation traceability rate, retrieval recall rate, knowledge version freeze rate, sensitive-data isolation rate, and failure-case ingestion rate.

3. Model Division of Labor and Experiment Tracking

General large language models handle idea generation, language conversion, and preliminary reasoning. Specialized verifiers handle mathematical checking, rule validation, and simulation validation. Retrieval systems provide evidence. Evaluation systems continuously monitor output quality.

Experiment tracking should at least record: problem ID, model and prompt version, retrieval evidence and library snapshot, proof-path ID, verifier and theorem-library version, verification result, manual revisions, timestamp, and resource consumption.

4. Infrastructure

Large-scale search and batch verification are suitable for container platforms running inference and verification tasks. Object storage holds datasets and experiment results. Message queues decouple task submission from execution. Logging services record the call chain. Monitoring and alerting track failure rate, resource utilization, and latency.

7. Risks and Compliance Statement (Important)

This article does not endorse any unverified scientific research claim. Until the original paper, preprint, or official announcement is available, the case above should be treated as an “unverified rumor.” Any citation must first verify the primary source and preserve links and version snapshots.

Three hard boundaries:

• Model output cannot automatically become a scientific conclusion. Important results require expert review, peer review, and independent reproduction.
• Formal verification passing does not mean the problem definition is correct. The stricter the verification, the more strongly it may reinforce a wrongly written direction.
• The responsible subject must be a human. When intellectual property, data security, or technology transfer is involved, the generation process and human contribution must be recorded, with a “human-in-the-loop” approach.

8. FAQ

What is a quantum complexity conjecture?
An unproven statement about the capability boundary between quantum and classical computing, such as whether a complexity separation exists for a class of problems or whether a quantum query lower bound holds.

How is an AI-generated proof verified?
Formalize it in a proof language such as Lean, Rocq, or Isabelle; confirm that it compiles without sorry and without undeclared axioms; then have experts compare the formalized statement with the original conjecture semantically.

Does quantum advantage equal universal superiority?
No. It depends on five conditions: problem-structure fit, resource-model clarity, noise and error correction, classical algorithm progress, and engineering reusability.

What are common enterprise mistakes?
Launching without a decision function; connecting only a large model but no verifier; failing to record versions and evidence; discarding failure samples; and promising theoretical results as product capabilities.

9. Summary

The technical lesson from this disclosure is not that “a certain model is stronger.” It is that the case points to a repeatable closed loop: problem formalization → knowledge retrieval → candidate generation → mechanical verification → failure attribution → human review.

For quantum computing, it reminds us that there are five hard conditions between theoretical boundaries and engineering implementation. For enterprise R&D systems, it suggests that the competitive focus is shifting from “model parameters and inference speed” to system capabilities: model + verifier + knowledge base + experiment platform + governance system.

Turning occasional “intelligence moments” into sustainable R&D productivity depends on versions, logs, reproducibility, and responsible ownership, not on the phrase “already cracked.”