A university group's autonomous research system published a disproof of Bandeira's matrix AM–GM problem at n = 5: a reduction to Lai–Lim's refutation of the Recht–Ré conjecture, an exact rational Farkas certificate for the semidefinite program behind it, and a Lean 4 formalization. Two gaps, both at the boundary the paper itself declares external: the claimant's certificate decides a different semidefinite program — the one its code wrote, without the polynomial transposes that make the Gram form a sum of squares — and the Lean development checks the certificate's arithmetic, not the program's infeasibility: no SDP is defined in Lean, and its impossibility theorems assume as fields what the certificate must deliver. The finite core is re-decided here with a certificate of our own, found in seconds and decided in exact rationals, so the conclusion stands.
The claim: github.com/Oxelra-AI/Bandeira-0.2a-open-source at commit c4137344 (MIT; 2026-06), its paper, its certificate (an npz of pickled object arrays, read inertly by opcode and never unpickled) and its Lean sources, all pinned by sha256 in corpus/bandeira/PINS.json. What is decided is the semidefinite program's infeasibility, from the SDP's definition in Lai–Lim (ICML 2020) as read here, with no code of the claimant's run; the Positivstellensatz step is a published theorem, cited. Pre-registered before any verdict (corpus/bandeira/preregistration.json). Nothing has been sent to the claimant.
| verdict | claim | how, and what is not decided |
|---|---|---|
| CERTIFIED | Lai--Lim's sum-of-squares SDP (Conjecture 1C, m = n = 5, Helton's form beta_a^T X_i beta_b) is infeasible at lambda = 120, hence lambda_2 > 120 = 5! | our own exact rational Farkas certificate (corpus/bandeira/certificate-cm.json; y0 = -1, denominators <= 10000, found by a float search and decided in exact rationals): m00 = -19/8568 < 0, the six 31 x 31 blocks positive definite by exact LDL^T, 120 y0 + b^T y = 1 > 0 |
| CERTIFIED | the claimant's certificate (y0 = -146/2061, y with denominators <= 10^4) is a Farkas certificate of infeasibility at lambda = 120 | for the SDP whose Gram form carries no transpose (beta_a X_i beta_b, the convention the claimant's export states and its Lean files encode); it is NOT a certificate for the sum-of-squares form under either transpose convention (the blocks lose positive definiteness) decided here under the claimant's convention: m00 = -1060/20438937 < 0, six blocks positive definite with the smallest pivots equal to the claimant's published ones, scalar 1417280/1417281 > 0; under leftT and rightT the same y fails the cone condition |
| CERTIFIED | Bandeira's Open Problem 0.2(a) for n matrices is the same inequality as Recht--Re's (RR_{n,n}) in spectral norm (the paper's Theorem 4.4) | by reading: Bandeira (2015) writes (a) as ||(1/n!) sum_sigma prod A_sigma(j)|| <= ||(1/n^n) sum_k prod A_k_j||; the right side is ||(A_1+...+A_n)^n|| / n^n by the distributive law, which is (RR_{n,n})'s with-replacement side with Lai--Lim's normalisation, and the left side is its distinct-index side; the paper's Lemma 4.1 (||S^k|| = ||S||^k for S PSD) is only needed for the form ||mean||^n. The Lean files state this reduction over an abstract ordered type (BandeiraAMGM.lean) and the identities concretely (ConcreteIdentities.lean); the Lean lane says whether they build. the two statements read side by side from the pinned sources (corpus/bandeira/sources/bandeira-open-problem-0.2_MIT18_S096F15.pdf, paper-main.tex, lai-lim-2020-pmlr-v119.pdf) |
| CERTIFIED | the Lean 4 development (Formalization/, the default Lake target, Lean v4.29.1 and Mathlib at the manifest's pin) states and proves what the paper's 'Lean formalization overview' lists: the equivalence 0.2(a) <=> (RR)_{n,n} over an abstract ordered type, the PSD spectral-norm power identity, the abstract scalar Farkas contradiction, the standard-form entry equalities Q = -M, six 31 x 31 blocks Q_b = L D L^T entrywise with positive pivots hence PosSemidef, and the 187 x 187 block-diagonal -M PosSemidef | by reading the theorem statements and the import graph at the pins (whether they compile is the 'lean' entry below, PENDING until lake build finishes); for the claimant's matrices, i.e. the SDP without the basis transposes (row bandeira-02a-claimant-certificate) every theorem statement of Core/, Farkas/, Bridges/, Certificate/FarkasStandard/ and the six Blocks/B*/B*FinalAsm.lean read against paper-main.tex; the import graph followed: AllBlocksFarkasChain imports the six FinalAsm and nothing imports AllBlocksFarkasChain; the NativePSD native_decide probes and the integer bound 144 > 120 (ConcreteIdentities.lean, native_decide) sit on the default target but on no theorem of the -M chain |
| CERTIFIED | Bandeira's Open Problem 0.2(a) is false for n = 5 | the finite core — the sum-of-squares SDP infeasible at lambda = 120 — is decided here by our own exact certificate; the step from that infeasibility to a PSD tuple violating the inequality is the noncommutative Positivstellensatz for bounded linear matrix-inequality domains (Helton--Klep--McCullough 2012, as Lai--Lim's Theorem 3 states it), a published theorem CITED and not re-derived, which the claimant's paper also declares external; the reduction from the inequality to the Loewner form and the equivalence with Bandeira's statement are read above; the Lean development certifies the claimant's certificate's arithmetic and not the SDP's infeasibility (row bandeira-02a-lean-reading), so nothing here rests on it. A claim whose analytic step rests on a cited theorem is certified with that step named, as the register does for Mathlib's theorems. composition of the rows above; the kinds of evidence are not merged |
Lai–Lim write the sum-of-squares side as tr(β X_i βᵀ Y_i) with β the column of basis monomials. A noncommutative square is fᵀ X_i f with f = Σ u_a β_a, and fᵀ X_i f = Σ u_a u_b β_aᵀ X_i β_b: the Gram form needs the first basis monomial reversed (X₁X₂ ↦ X₂X₁), which the notation βᵀ carries silently. The claimant's builder (corpus/bandeira/sources/lailim_sdp.py.txt, read as text) forms β_a X_i β_b with no reversal. That is a different linear map from Gram matrices to polynomials, so its Farkas certificate is a certificate of a different program.
| certificate | fᵀ X f, left transpose | right transpose | no transpose |
|---|---|---|---|
| the claimant's (y₀ = -146/2061) | REFUTED | REFUTED | CERTIFIED |
| ours (y₀ = -1) | CERTIFIED | CERTIFIED | REFUTED |
Under its own convention the claimant's certificate holds exactly as published: m₀₀ = -1060/20438937, scalar 1417280/1417281, and the smallest LDLᵀ pivot of each block equal to the one its verification summary prints. The same multipliers under the sum-of-squares form lose positive definiteness in every block. The claimant's paper calls the identification of its matrices with Lai–Lim's SDP the one component outside its Lean proof; this is what sits there. The optimum of the two programs coincides in floating point on every case tried (§3), so the finding is about what the published certificate decides, not about the theorem.
| (m, n) | λ₁ / λ₂, left transpose | right transpose | no transpose | Lai–Lim | n!/(n−m)! |
|---|---|---|---|---|---|
| (2, 2) | 2.0000 / 0.5000 | 2.0000 / 0.5000 | 2.0000 / 0.5000 | 2.0000 / 0.5000 | 2 |
| (2, 3) | 6.0000 / 1.5000 | 6.0000 / 1.5000 | 6.0000 / 1.5000 | 6.0000 / 1.5000 | 6 |
| (3, 3) | 6.0000 / 3.4113 | 6.0000 / 3.4113 | 6.0000 / 3.4113 | 6.0000 / 3.4113 | 6 |
| (4, 4) | 24.0000 / 22.4746 | 24.0000 / 22.4746 | 24.0000 / 22.4746 | 24.0000 / 22.4746 | 24 |
| (5, 5) | — / 144.6488 | — | — / 144.6488 | — / 144.6488 | 120 |
Floating point (cvxpy, SCS at 10⁻⁸), shown as a measurement: for m ≤ 3 the conjecture is a theorem, so λ₁, λ₂ ≤ n!/(n−m)! must hold, and does, under every convention. The verdict rests on the exact certificates of §1 and §2, never on these numbers.
What the files state, and the paper lists: the equivalence 0.2(a) ⇔ (RR)ₙ,ₙ over an abstract ordered type (Core/BandeiraAMGM.lean), the spectral-norm power identity (Core/SpectralNormPSD.lean), the abstract scalar Farkas contradiction (Farkas/AbstractFarkas.lean), 5,766 standard-form entry equalities Q = −M by norm_num (Certificate/FarkasStandard/FarkasStandardFull.lean), six 31 × 31 blocks Q_b = L D Lᵀ row by row with positive pivots, hence PosSemidef (Certificate/Blocks/B*/), and the 187 × 187 block-diagonal −M PosSemidef (Farkas/AllBlocksFarkasChain.lean: negM_full_posSemidef). All of it for the claimant's matrices — the SDP of §2 without the transposes.
What they do not state: a definition of Lai–Lim's SDP, or a theorem that any SDP is infeasible. The two impossibility theorems — no_lailim_feasible_from_certificate_semantics (Farkas/SDPFarkasSemantics.lean) and no_native_farkas_feasible (Bridges/NativeFarkasAdapter.lean) — are IsEmpty of structures whose fields assume the standard-form pairing pairM = y₀c₀ + lin, the cone inequality or (−M) ⪰ 0, the bound c₀ ≤ 120 and the scalar inequality; negM_full_posSemidef is never supplied to either, nothing imports AllBlocksFarkasChain, and GeneratedFarkasTheoremShape takes three arbitrary Props as hypotheses. The docstrings say it: "the remaining work is to fill GeneratedCertificateAdapter from the actual generated theorem families rather than by assumptions." So Lean checks the certificate's arithmetic — which §2 also checks here, exactly, in two implementations — and the identification with Lai–Lim's program, the step §2 finds wanting, is outside Lean, as the paper's boundary section says of C_i and b. Its abstract says "the entire certificate" and its overview names "an SDP infeasibility semantic bridge".
Smaller, at the pin: Tests/UnformalizedDependencies.lean still lists the spectral-norm power identity as unformalized while Core/SpectralNormPSD.lean proves it, and calls the integer bound 144 > 120 "floating-point and NOT a rigorous bound" — that bound is proved by native_decide and is not load-bearing. native_decide (trust in the compiled evaluator, axiom Lean.ofReduceBool) appears on the default target in the NativePSD probes, a test file and that bound; on no theorem of the −M chain.
Build: the default Lake target (439 sources, Lean v4.29.1, Mathlib at the manifest's pin) is being built here; the slow tail is the NativePSD probes evaluating 31 × 31 rational LDL factors with native_decide. When it finishes, the axioms of the four theorems above are asked of the kernel and recorded in corpus/bandeira/lean-build.json; this paragraph then says what came back. Nothing on this page rests on the build.