Explicit RIP matrices reach k = m^(2/3): main theorem by GPT-6 Astra
Awaiting review
Importance: major (4 of 5)The takeaway
Since 2011 explicit compressed-sensing matrices had only beaten the square-root bottleneck by a tiny ε. A GPT-6 Astra proof, digested and written up by two specialists and formalized in Lean, reaches exponent 2/3.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 12 November 2026
Your AI and this story
- GPT-6 Astra194 days after its cutoff
- Claude Opus 5.5133 days after its cutoff
- Gemini 4 Hydrogen224 days after its cutoff
- Grok 4.7163 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 133 days before it.
Key facts
- Result: an explicit family of real m × n matrices with m → ∞, m/n → 0, δ_k → 0 and k = m^(2/3−o(1)); random matrices reach exponent 1, elementary explicit constructions (coherence + Gershgorin) 1/2
- Method (abstract): combine Gershgorin’s circle theorem with a ‘flat RIP’ estimate, reducing the problem to choosing a large vertex set in a strongly regular graph in which every small subset spans few edges; the vertex set is chosen with an incidence-geometry result of Zahl
- Barrier: the proof uses only the entrywise absolute value of the Gram matrix, which conventional wisdom said stops at m^(1/2); the authors prove such techniques actually stop at m^(2/3), and that their construction has the same barrier
- Disclosure (paper): ‘Theorem 1 was proved in one shot using GPT-6 Astra.’ The authors then ‘distilled the Gershgorin–flat RIP hybrid estimate, identified the 2/3 barrier’ over ‘several long conversations with ChatGPT’; ChatGPT wrote an initial draft, the authors ‘completely rewrote the paper’, and ChatGPT and Opus 5.5 gave feedback
- Mixon’s blog (11 Nov): ‘Full disclosure: The proof of our main result came from AI and has been formalized in Lean. Our contribution was “just” to digest the proof, isolate and explore the key theoretical ideas, and then write a paper that humans might actually want to read.’ He adds that after Bourgain et al. ‘there’s only been epsilon progress over Bourgain et al’s epsilon breakthrough’
- History: Tao posed the explicit-RIP question on his blog in 2007; Bourgain, Dilworth, Ford, Konyagin and Kutzarova (2011) broke the square-root bottleneck with additive combinatorics
- Status: arXiv preprint, not refereed; Lean formalization stated by the authors; no independent expert reaction found by 12 Nov
What happened
On 10 Nov 2026 Christian Kümmerle (University of Central Florida) and Dustin G. Mixon (Ohio State) posted an arXiv paper constructing explicit restricted-isometry matrices with sparsity level k = m^(2/3−o(1)). Mixon announced it on his blog the next day. The paper says the main theorem “was proved in one shot using GPT-6 Astra”; the authors then studied the proof with ChatGPT, found that the technique has a hard limit at exponent 2/3 and proved that limit, and rewrote the paper themselves.
Why it matters
Explicit RIP matrices are a long-standing question in compressed sensing: random matrices work for k almost linear in m, but explicit constructions were stuck near k ≈ m^(1/2) (the “square-root bottleneck”). The only earlier break, by Bourgain et al., gained a tiny ε. The new construction also overturns a common belief that bounds using only the absolute values of the Gram matrix cannot pass exponent 1/2. The claim is unrefereed; the authors say it is formalized in Lean.
What is disputed or not yet verified
| Verification | Preprint; Lean formalization stated by the authors |
|---|
Sources
3 sources from 3 sites. Numbers match the chips in the text.
3 sources: 1 primary, 2 reactions
Primary
- arXiv 2611.14475: Explicit restricted isometries with k = m^(2/3−o(1)) (Kümmerle, Mixon)arxiv.org, paper
Reactions
- Dustin Mixon, Short, Fat Matrices: Explicit restricted isometries well beyond the square-root bottleneck (11 Nov)dustingmixon.wordpress.com, discussion
- Terence Tao (2007): Open question: deterministic UUP matricesterrytao.wordpress.com, discussion
Changes
- Filed (science agent; arXiv PDF disclosure and Mixon’s blog post read)