That is what Denise Holt and Denis Ovseyenko of AIX Global report in “Demonstrating Quantum Value by Solving the Six Remaining Clay Millennium Problems.” They say IBM Heron computations produced certificates carried into Lean 4, yielding 27 theorems from 10 hours 24 minutes of QPU time.
I have not verified those claims, and the Clay Mathematics Institute still treats the six problems as unsolved. I am not asking you to accept the proofs. I am asking why the same architecture appears to have surfaced twice.
More than two months before the AIX preprint, my Six Birds Theory paper “One Meta-Theory, Three Clay-Problem Closures” reached a related structural conclusion from the opposite direction. It compared Navier–Stokes, the Riemann Hypothesis, and P versus NP and argued that they share a grammar: representation, residual obstruction, missing content, bridge, and audit.
One program started with a theory of emergence and moved toward hard problems. The other says it started with the problems separately and found one computational pipeline.
They do not offer the same proof. They appear to have found the same kind of bottleneck.
In software terms, think of a mathematical layer as an API. It exposes certain objects and operations. You can optimize forever inside that interface, but you cannot recover a distinction it never exposes. If two states produce the same log but need different responses, more log processing will not fix the observability problem. You need a new sensor, richer representation, or theorem showing the distinction does not matter.
Six Birds Theory formalizes this through saturation and residuals. Repeating a fixed completion rule is not the same as gaining new access. A residual measures the part of the target not accounted for by the layer’s native probes. A useful extension constrains that residual, then returns only what the original question needs.
That resembles the architecture AIX claims to implement:
native problem -> problem-specific operator -> governed quantum computation -> compact certificate -> classical proof checker
The quantum state need not be reconstructed classically. The receiving layer needs a sufficient certificate and a valid bridge to the theorem.
There is one exact point of contact. In the Hodge section, AIX constructs a defect object measuring what remains after algebraic cycles account for the Hodge-class space. My earlier paper “Adequacy Residuals and Blind-Spot Currency” generalizes the same job: remove what the available probes explain and measure the remainder. Under the Hodge choices, the constructions have the same operator form.
That does not mean AIX used my work; I have no evidence of that. The mathematics is classical. It means two programs, with different vocabularies, built a tool for the same structural job.
“One mechanism” should not mean “one equation.” Riemann and Yang–Mills concern confinement. Hodge and BSD compare presentations. Navier–Stokes asks for global control. P versus NP asks whether an obstruction persists against every efficient procedure. Same grammar, different polarity.
The developer lesson is broader. AI systems, theorem provers, and scientific workflows increasingly perform opaque searches. The right design target may be the smallest independently checkable artifact that preserves why the answer is true.
I wrote the full comparison, chronology, and caveats in Two Roads to the Same Bottleneck.
Disclosure: I developed Six Birds Theory and lead Automorph. This is a structural comparison, not validation of AIX’s claims.