Scott Aaronson and Andris Ambainis published their conjecture in 2008. It survived eighteen years, several partial results and a great deal of attempted machinery. On Nov. 6, Physical Superintelligence, a research group in San Francisco, said a system it built had a complete proof by the third day of a run, and that Lean, a proof assistant that checks every inference against formal rules, accepted it. The question the conjecture settles is narrow and consequential. Quantum computers beat classical ones on problems with hidden structure, as Shor’s factoring algorithm showed in 1994: the input repeats, and the quantum machine finds the period. Whether a quantum computer can be exponentially faster on a random input, which almost never has structure, was open. Aaronson and Ambainis reduced that to a statement about polynomials and showed that if the statement holds, quantum machines are at most polynomially faster on random inputs. Proving it means establishing a limit on what quantum hardware can ever do to a class of problems that has no pattern to exploit.
The run itself was ordinary in the way that matters. PSI’s system ran on the group’s own infrastructure, using instances of a non-public Anthropic model. It improved the result twice during the run, and Lean accepted the final version. The proof builds on work by Shachar Lovett and Jiapeng Zhang on polynomial methods, on results of David Reimer, and on a proof of the van den Berg-Kesten conjecture, which is the kind of lineage that suggests the argument arrived by extending existing tools rather than by inventing a new field.
What separates this from most claims of the past two years is that a stranger can check it. The group published the paper and the code, and Lean does not care who wrote the proof or what the author’s incentives are. That is a different standard from the one applied to a language model that announces a theorem and withholds the manuscript, which has become a familiar pattern: a claim circulates as reputation, is cited in fundraising conversations, and cannot be examined by the people best placed to find the error. The mathematicians closest to the problem have been reading it. In August, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford settled the conjecture’s prediction in a special case, for quantum algorithms that read their input in a fixed number of parallel rounds. They have since gone through the full proof, sent comments, and are writing a shorter exposition for experts. Their assessment, as PSI relayed it, is that the result resolves a decades-old conjecture and draws together several lines of work in the analysis of Boolean functions and probabilistic combinatorics in a way that looks almost magical.
The same week brought a claim of a different kind. METR, a research organization that studies AI capabilities, published an eleven-week investigation concluding that AI-assisted research inside Anthropic had roughly doubled the rate at which the company’s models improve, compared with a year earlier. The company removed or redacted most of the key evidence in the report, citing commercial sensitivity. The finding may well be right. It cannot be audited, because the data that would establish it sits behind a corporate decision. The two stories are usually told as one: models are getting better at doing research, and here is the evidence. Read closely they are separate. One produced an artifact that a machine can verify and a stranger can read. The other produced a conclusion whose supporting material the subject of the study controls. The first is knowledge. The second is a press release with a methodology attached, and the difference is not about honesty but about where the evidence lives.
The recursion argument underneath is the interesting one. If a lab uses its own models to accelerate its own research, the improvement compounds, and the entity best positioned to measure that compounding is the lab. Outside evaluators get a snapshot, on terms the lab sets, after the lab has decided what counts as proprietary. That is a structural problem, not a scandal. It is the same problem regulators have with banks measuring their own risk models, and it has the same remedy: independent access to the underlying data.
The commercial stakes are not incidental. Anthropic is preparing a listing at a valuation in the trillions, and a settled conjecture is a credential that survives scrutiny in a way a benchmark score does not. Every lab has saturated the standard tests. Research mathematics is one of the few fields where a result cannot be dismissed as contamination, because the artifact either checks or it does not. That makes a theorem worth more to a roadshow than a hundred percentage points on a leaderboard.
For the field, the more useful outcome is a template. Publish the proof, publish the code, let the checkers work, and accept that the process will take months and may return a no. In this case it returned a yes in three days of machine time and an unknown number of human hours before that, which is itself a number worth having and is not in the release.
The question that remains is the one a proof does not answer. A system that can close an eighteen-year-old problem in three days is doing something real. Whether it can find its own mistake, or whether that still requires a person who understands the subfield well enough to suspect the lemma on page forty, is a different measurement, and nobody has run it.
