AIX Global Innovations Claims to Have Solved All Six Millennium Prize Problems. Its Own Lean Audit Says Otherwise.

On August 30, AIX Global Innovations uploaded a 54-page paper to Zenodo titled “Demonstrating Quantum Value by Solving the Six Remaining Clay Millennium Problems.” The authors: Denise Holt and Denis Ovseyenko, the same two founders whose fault-tolerant quantum computing claim I analyzed in June and found to be a post-selection and classical optimization pipeline operating at code distance 1, where no quantum error correction is possible.

AIX Global Innovations claims to have solved the Riemann Hypothesis, the Yang-Mills existence and mass gap problem, the Navier-Stokes existence and smoothness problem, the Hodge conjecture, the Birch and Swinnerton-Dyer conjecture, and P ≠ NP. All six remaining Clay Millennium Prize Problems. On rented IBM Heron hardware. For a reported total of $59,904 in cloud computing time.

They did not.

On September 1, AIX released the Lean 4 package it said would let anyone verify the results. I examined it. The package does not contain six closed proofs of the six Clay problems. AIX’s own included audit tool confirms this. To be direct: these problems have not been solved. The Lean package proves conditional implications (“if these premises hold, then the theorem follows”) and leaves the hard mathematics in unverified premises attributed to a proprietary oracle. That is not what solving a Millennium Prize Problem means.

What the Package Actually Shows

The paper claims six closed *_final theorems, each inhabiting the bare official type of the corresponding Clay problem with no remaining premises. The released package designates a different set of declarations as its six final results. It ships with an audit.py script whose committed output tells the story:

Four of six are conditional. The decisive mathematics in each case lives in the premises (hD, corr, hc, hid, hlb, bridge), which are described as outputs of the proprietary “governed spectral oracle” but are not proved in the package. Lean checks the implication from those premises to the conclusion. The premises themselves are unverified.

The two marked CLOSED are worse than they sound. The Navier-Stokes entry, ns_official, is a def, a definition of the proposition that would need to be proved. In Lean 4, defining a proposition and proving it are different things. Creating the type is the statement; inhabiting the type is the proof. The Hodge entry, hodge_kunneth, proves that convolution of the lists [1,1,1,1] and [1,1,1] produces [1,2,3,3,2,1]. That is a true and trivially checkable arithmetic fact about the Hodge numbers of CP³ × CP². It is not the Hodge conjecture, which asserts something about every smooth projective complex variety.

The paper claims separate, fully closed riemann_final, yang_mills_final, navier_stokes_final, hodge_final, bsd_final, and p_neq_np_final theorems exist. The released package does not identify these as its final results. Its own audit table lists the conditional and definitional objects above.

What Lean 4 Verifies and What It Does Not

Lean 4 is a legitimate and well-respected proof assistant. Its kernel checks that a proof term inhabits the claimed type. If it does, the logical chain from premises to conclusion is sound.

AIX emphasizes that #print axioms reports no sorryAx and no project-specific axioms for any of its finals. That is true and irrelevant. Lean’s axiom report tracks which foundational axioms a declaration transitively uses. It does not report ordinary premises that appear in the theorem’s type signature. A theorem of the form “given a proof of P, P is true” has a clean axiom report. It still does not prove P.

Lean’s own documentation on validating proofs separates two questions: Has Lean accepted a proof of the formal theorem statement? And does the formal statement actually mean what its author claims? The documentation warns that statement meanings and referenced definitions must be independently examined, and recommends external checkers for high-stakes or potentially misleading proofs.

AIX’s audit.py accidentally makes this distinction visible. Four of the six finals carry explicit premise binders. Those premises are where the Clay-problem-solving mathematics would need to live. Naming them “committed spectral certificates” does not turn them into proved terms. The Lean layer checks the reduction from premises to conclusion. The released package does not show that the premises themselves have been established.

The Same Debunked Foundation

The paper builds directly on the FTQC paper I analyzed in June. It cites it as reference [1] and states the two “should be read as a pair.” Between the two, AIX also published a hydrogen chain paper on August 27, claiming to have computed exact ground-state energies for hydrogen chains up to H₁₀₀ using the same architecture, framed as “beyond the reach of classical computing.” Three papers in ten weeks trace a clear arc: FTQC on small molecules in June, exact hydrogen chain energies “beyond classical reach” in August, all six Millennium Prize Problems by the end of August.

All three papers use the same d=1 register, the same “admissibility envelope,” the same “twelve decimal places” agreement, the same “self-certified fixed point” language, and the same classical Newton projection that I showed in June produces the twelve-decimal agreement as a property of the optimizer rather than of quantum error correction. All three claim “no error mitigation, post-selection, or classical fitting,” despite the companion FTQC paper documenting all three.

All six deciding spectral computations are described as running on 156-qubit IBM Heron r3 systems via the cloud. IBM has not acknowledged or commented on these results, just as it did not acknowledge the June FTQC claim.

Three Problems, One Template

AIX’s own Lean 4 code reveals that three completely different mathematical problems produce the identical two-line proof:

Navier-Stokes (fluid dynamics): theorem navier_stokes (step : ∀ n, Tower.declInv n → Tower.declInv (n+1)) : ∀ n, Tower.declInv n := Tower.universal step

Hodge (algebraic geometry): theorem hodge (step : ∀ n, Tower.declInv n → Tower.declInv (n+1)) : ∀ n, Tower.declInv n := Tower.universal step

BSD (number theory): theorem bsd (step : ∀ n, Tower.declInv n → Tower.declInv (n+1)) : ∀ n, Tower.declInv n := Tower.universal step

Three problems from three different branches of mathematics, each reduced to the identical template. Tower.declInv and Tower.universal are custom definitions in AIX’s package, not standard mathlib objects. The step hypothesis is where the actual mathematics would need to live, and it is described as being “discharged by GFTQC,” the proprietary oracle.

This kind of definitional problem has precedent. In a separate case in June 2026, a GitHub issue opened the day after an advertised Lean 4 proof of P = NP showed that the project’s top-level proposition had been defined as True in its initial version and later revised to an uninterpreted axiom, never formally connected to actual complexity classes. Definitional sleight-of-hand in Lean 4 type definitions is a known failure mode, and the defense against it is independent audit of the definitions. AIX’s custom Tower namespace has not been audited by anyone outside the company.

The Universal Quantifiers Are Where the Proof Disappears

The Riemann Hypothesis is a statement about infinitely many zeros of the zeta function. Navier-Stokes is about every smooth initial condition for all future time. Hodge covers every smooth projective complex variety. BSD applies to every elliptic curve over the rationals. P ≠ NP is a statement about every possible polynomial-time algorithm.

Every conventional mathematical proof is a finite object, and finite proofs routinely establish statements about infinite sets. Euclid’s proof covers infinitely many primes. An induction proof covers every natural number. A finite Lean 4 term can prove a universally quantified proposition. That is not the issue.

The issue is whether AIX has supplied a checkable argument covering each universal quantifier. In each case, the universal bridge is the missing object. For Riemann, the correspondence corr that maps every nontrivial zero to a spectral point. For P ≠ NP, the all-algorithm transfer bridge bridge that converts every polynomial-time decider into a bounded-size refutation. For BSD, the rank-order equality over every elliptic curve. The paper calls each of these a result of governed computation. The released Lean package leaves every one of them as a premise.

AIX’s Cost Table

AIX provides a cost table pricing each Clay problem at IBM’s metered rate. The Riemann Hypothesis: 18 minutes, $1,728. The Hodge conjecture: 14 minutes, $1,344. P ≠ NP: 2 hours 31 minutes, $14,496. Total for all six: 10 hours 24 minutes, $59,904.

These six problems have resisted the combined efforts of the world’s best mathematicians for over 25 years. They carry $6 million in Clay Mathematics Institute prize money. AIX Global Innovations prices their resolution at under $60,000 of rented cloud time.

The Cost to Real Science

Quantum computing is at a fragile stage. Real progress is happening. Google, IBM, Quantinuum, and academic groups around the world are doing difficult, incremental, peer-reviewed work toward fault tolerance and practical quantum advantage. That work depends on public trust, investor confidence, and policymaker understanding that quantum computing is a serious scientific and engineering discipline.

Papers like AIX’s corrode that trust. When a company with no peer-reviewed publications in mathematics or quantum information claims to have solved the six most celebrated open problems in mathematics for the cost of a conference registration, and the claim appears on Zenodo with a DOI that gives it the appearance of scientific literature, it damages the credibility of the entire field. Zenodo assigns DOIs automatically to published records; a DOI means a record is persistent and citable, not that its contents have been peer-reviewed or endorsed.

I have been warning about this dynamic for months. The gap between quantum hype and quantum reality is where the quantum winter begins, and AIX Global Innovations is widening that gap faster than almost any company I have covered.

The Quantum Snake Oil Dictionary documents the general patterns. The vendor deflection playbook catalogs the responses. AIX’s “Demonstrating Quantum Value by Solving the Six Remaining Clay Millennium Problems” is one of the most extreme example I have encountered of both.

What Would Constitute Evidence

AIX’s Lean source is now released. A few questions:

Do the six *_final declarations claimed in the paper actually exist in the released package and inhabit faithful formal statements of the six Clay problems without local premises? Do AIX’s custom definitions (Tower.declInv, Tower.universal) express the same propositions as the official problem statements? Are the supposedly quantum-generated certificates (corr, hlb, bridge) present as kernel-checkable proof terms, or as parameters accepted by conditional theorems? Can independent specialists reproduce the claimed spectral computations from disclosed inputs, job records, and algorithms?

A clean lake build would establish that Lean accepts the declarations in the package. It would not, by itself, answer those semantic and scientific questions. Lean’s own documentation says the theorem statement and every referenced definition must be examined when there is doubt about what a result means.

The Clay Mathematics Institute’s process comes later. However, CMI does not accept direct submissions – proposed solution must first be published in a qualifying outlet, survive at least two years of scrutiny, and achieve general acceptance in the global mathematical community. As of September 2, CMI continues to list all six problems as unsolved. Nothing in AIX’s paper or package has a chance at changing that status.

The six Clay Millennium Prize Problems remain open. What AIX has produced is Lean-checked conditional reductions, custom definitions, and finite examples wrapped around six famous problem statements. The hard mathematics, in every case, has been placed into a premise and attributed to a proprietary computation that runs on an architecture I have already shown does not do what it claims. Calling that “solving” the Millennium Problems is like writing “assume P ≠ NP” at the top of a page and calling the rest a proof.