PSI reports AI proof of Aaronson–Ambainis conjecture | Magica
PSI reports AI-found proof of Aaronson–Ambainis conjecture
Editorial Team
••📖7 min read
Physical Superintelligence says its AI system found a proof of a conjecture limiting quantum query advantages on random inputs. Public proof files enable scrutiny, but do not establish the private system’s cost or repeatability.
PSI says its research system found a proof during the third day of a run using a non-public Anthropic model.
The claimed result limits exponential quantum advantages on most uniformly random inputs in the query model.
Public verification files support scrutiny; experts must still check that the encoded statement captures the conjecture.
Physical Superintelligence (PSI), a Cambridge, Massachusetts-based startup building AI systems for physics research, announced on November 6 that its internal research system had found a proof of the Aaronson–Ambainis conjecture, open since 2008. The company has released a manuscript and a formalization in Lean 4, a proof assistant that checks mathematical arguments by computer.
The result addresses when quantum computers can gain an exponential advantage in accessing input data. For PSI, which launched publicly in September with $58 million in announced seed funding, it is also evidence offered for a business built around AI conducting research under human direction. The public files allow scrutiny of the finished mathematics; they do not reproduce the private system’s discovery process.
What the result would settle
Computer scientists Scott Aaronson and Andris Ambainis formulated the conjecture about bounded, low-degree polynomials to investigate the need for structure in quantum speedups. Their original paper, published in 2014, works in the black-box model and establishes a conditional consequence: if the conjecture holds, a quantum algorithm making T input queries can be simulated on most inputs with a number of classical queries polynomial in T.
That scope matters. Query complexity measures access to input data; it is not a benchmark of total computing time or a comparison of commercial quantum hardware with ordinary computers. The result therefore does not establish that classical machines can efficiently replace quantum computers for every task.
PSI’s announcement explains the mechanism. A classical query reads one input bit; a quantum query can access positions in superposition. After T quantum queries, the probability of answering yes is a polynomial of degree at most 2T in the input bits, bounded between zero and one. The conjecture says that, provided this polynomial has meaningful variance, at least one input bit must have substantial influence on its value.
Internet scans and leaked databases expose the spread of ARTEX, a security-testing framework used in cyberattacks. Researchers documented largely autonomous compromises, but the records also show failed cashouts and uncertain counts of independent deployments.
Editorial Team
An ordinary computer that knows the polynomial can inspect influential bits until the remaining uncertainty is small, then estimate the quantum algorithm’s probability of answering yes. For fixed approximation error and a fixed fraction of excluded inputs, the required number of queries grows polynomially rather than exponentially in T. The guarantee concerns most uniformly random inputs, leaving room for exponential speedups on appropriately structured problems, such as those exploited by Shor’s factoring algorithm.
The released repository states a quantitative bound: for a polynomial of degree at most d, taking values in [0,1] and having variance at least ε on uniformly random bit strings, some bit has influence at least
(8√15 / (125π⁴)) × ε^(5/2) / d⁶ ≥ (ε/d)⁷.
Here influence is the squared change in the polynomial when that bit is flipped, averaged over inputs. The significant improvement is the polynomial dependence on degree: PSI says previous general bounds decayed exponentially in degree.
A new argument built on earlier work
PSI’s claim is a general result where earlier work had settled special cases. Its announcement notes that the influential-variable conjecture was already known for polynomials taking only the values zero and one, alongside other restricted cases. The new result covers polynomials whose values may lie anywhere between zero and one.
The proof also extends an existing research programme. PSI credits the fractional-certificate approach of researchers Shachar Lovett and Jiapeng Zhang, whose 2023 work left a key inequality conjectural. The new argument substitutes another inequality, using a determinant to pair input settings while controlling how often paired settings agree on individual coordinates. That strengthens a pairing supplied by David Reimer’s Butterfly Lemma.
There was also recent progress on the computational consequence. In August 2026, Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan established the simulation result for quantum algorithms restricted to a fixed number of parallel rounds. According to PSI, they have been reading the full proof, sending comments and preparing a shorter exposition for experts. Their favorable assessment appears in PSI’s announcement; it is an attributed expert response supplied by the company.
Public mathematics, private discovery system
PSI describes itself as an AI-native physics laboratory organized as a public benefit corporation. In its September 1 launch announcement, it announced the $58 million seed round led by Breakthrough Energy Ventures and plans to turn part of its platform into a product for optimizing terrestrial and orbital data centers. That gives the research claim a commercial context, although this proof provides no measurement of data-center performance.
A report describing PSI’s earlier releases says the company published claimed solutions to five problems from the Open Quantum Problems list in October, each with a paper and Lean formalization. It also describes PSI’s open-source agentic physics tool, Get Physics Done. The company thus has earlier public research artifacts, while the system behind this proof remains internal.
David Turturean, a member of PSI’s technical staff who developed its research system, led the work. PSI says he scoped the problem, ran the system, prompted the model to package the results into a first draft and reviewed that draft. He accepts responsibility for the paper’s correctness. Company advisors Jim Halverson and Phiala Shanahan respectively audited the proof and commented on the formalization.
The repository discloses that AI models produced the mathematical statements, first paper draft and Lean formalization. PSI says the system found a complete proof during the third day of a run on its own infrastructure, then improved the result twice while working on related problems.
The announcement identifies the model supplier as Anthropic, the AI developer, but does not identify the non-public model or disclose the run’s compute budget or cost. That prevents a cost comparison with other research methods.
PSI’s company-reported memory use for concurrent and sequential proof verification. These figures measure checking the proof, not discovering it. Source: PSI proof repository.
What still needs checking
The repository reports no proof placeholders or added axioms in the formal development, while listing standard Lean principles used through Mathlib, its mathematical library. Its verification records describe replay through Lean’s kernel and an independent implementation, lean4lean, plus a sandboxed comparator using Lean and the Rust-based nanoda checker. Independence here concerns checker implementations.
The repository also reports a useful control: a small project in which a false statement was added with the kernel switched off passed a build and axiom report but was rejected by both replay checkers. That illustrates why the published verification goes beyond a successful build.
Rechecking has a disclosed resource footprint. The repository reports that concurrent module replay used 173 GB of memory on an eight-core machine. Running modules sequentially used 7.4 GB and took 11 minutes. Those figures describe verification configurations, not the compute or time needed to discover the proof.
There is an important distinction within the published results: the main conjecture is presented without an additional hypothesis, but a fourth theorem offering an improved constant assumes a separate degree bound that is not formalized in the project. That conditional improvement should not be conflated with the unconditional main result.
The limits are explicit in both the repository and a technical account of the release. A human reader must confirm that the formal definition expresses the printed conjecture. The manuscript itself is not machine-checked, including passages on consequences and earlier work. The checkers also rely on their underlying software, mathematical definitions and hardware.
The next substantive test is expert examination of that correspondence and of the paper’s interpretation. PSI has made the proof available for that scrutiny. Whether its private research system can deliver comparable results repeatedly, and at what expense, remains a separate question that this release does not resolve.
Meta's strategy chief and former CFO is joining Fireworks AI ahead of a reported fundraising push targeting at least a $30 billion valuation. The inference company announced a $17.5 billion valuation in July, making the hire part of a much larger expansion than its older funding figures suggest.
Sand.ai says its $200 million Series A+ round lifts its valuation above $1 billion. Co-lead investor Wangsu plans inference and deployment cooperation, while its filing shows substantial losses behind the startup’s video AI ambitions.
An advocacy group estimates Interior Secretary Doug Burgum’s AI holdings at $18.1 million–$64.4 million as his department advances data centers on public land. His ethics agreement allows retained investments with recusals, while pending permits will determine both the application of those safeguards and the public’s return. Interior denies his decisions are driven by personal investments.
Microsoft is evaluating fewer neocloud partners while expanding its own infrastructure. Delivery-dependent contracts underpin supplier financing, while IREN reports rising revenue alongside a $6 billion funding target for its broader expansion.
OpenAI is expanding its relationship with Hacktron, whose researchers previously reported an attack chain into employee accounts, to test third-party connections with greater access to cybersecurity models.
Google has acquired Crusoe’s southeast Wyoming data center site, where it plans a long-term $17 billion investment. Crusoe describes completed pre-development work; independent reporting points to customer setbacks. Power delivery and carbon capture remain key tests.
The team behind document-parsing service SoMark has released OXR-1.0 code and weights. A benchmark retest supports a strong result, but speed and accuracy were measured separately, and users above funding or revenue thresholds need a commercial license.
OpenAI is reportedly developing a Business Hub with daily mention and click charts, product updates and business agents. The unannounced feature could give verified businesses direct visibility into ChatGPT responses, without revealing prompts or competitor rankings.
Palantir and Nvidia have specified an integrated stack for running AI in customer-controlled environments. The architecture builds on existing software and infrastructure offerings, with published configurations spanning 32 to 640 GPUs, while pricing and workload economics remain unproven in the launch materials.
Democrats’ incoming congressional majorities put hearings and investigations within reach, but AI rules and crypto legislation still face bipartisan bargaining and a Republican president.
Microsoft reportedly declined to renew Oracle server rentals as older chips became less useful to it. The decision comes despite continuing capacity shortages, while Oracle says demand for earlier-generation GPUs remains strong.
An investigation puts Nvidia’s future commitments and guarantees at $530.5 billion. Its disclosures show rapidly expanding supplier commitments and phased support for customers whose infrastructure could generate further chip sales, with cash payments depending on timing, demand and contract terms.
TSMC is reportedly planning a possible move into 3D DRAM at Nvidia’s request. The foundry already helps integrate AI processors with memory, but a manufacturing expansion has no disclosed factory or production date.
Physicl has raised a $10 million seed round and introduced Studio, a beta app for generating targeted physical AI data. Its reported customer gains concern 3D reconstruction, leaving broader robot reliability and commercial economics to be demonstrated.
New cloud partners in Southeast Asia must enroll in Nvidia’s Fleet Intelligence system, according to a report, linking preferred chip access to monitoring while leaving data sharing and existing partners’ obligations unresolved.
Airbnb sold intellectual property to a private AI lab controlled by CEO Brian Chesky in a $7.1 million arrangement that also reimburses expenses. It obtained a license to certain lab technology and future investment rights, but disclosed no asset valuation or detailed license terms.
Chip shares recovered part of Thursday’s losses in early Friday trading. Fears about data-centre construction face a test against AI-chip supplier Nvidia’s strong reported sales, growth forecast and conditional infrastructure-financing plans.
SoftBank shares fell 10.8% as default-insurance costs reached a four-year high. Delayed listings and unfinished data centers complicate its AI investment outlook, while a $40 billion bridge facility has a March 2027 maturity and a repayment plan based on existing assets and other financing.
U.S. prosecutors allege a global fraud combined AI impersonation, sham confidential deals and cryptocurrency laundering. A blocked bank transfer shows why convincing an employee and moving the money are separate hurdles.
