--- id: "2026-11-10-explicit-rip-matrices-two-thirds-gpt-6-astra" url: "https://postcutoff.com/e/2026-11-10-explicit-rip-matrices-two-thirds-gpt-6-astra/" as_of: "2026-11-13T13:49:00+01:00" date: "2026-11-10" date_precision: day category: science importance: 4 confidence: medium status: [Awaiting review] verification: Lean-verified sources: 3 editor: human editor human_review: null version: "2026-11-12" --- As of: 2026-11-13 13:49 CET. Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/ Canonical page: https://postcutoff.com/e/2026-11-10-explicit-rip-matrices-two-thirds-gpt-6-astra/ # Explicit RIP matrices reach k = m^(2/3): main theorem by GPT-6 Astra Full title: Explicit restricted isometries with k = m^(2/3−o(1)): Kümmerle and Mixon say GPT-6 Astra proved the main theorem 'in one shot', far past the square-root bottleneck of compressed sensing arXiv 2611.14475 (submitted 10 Nov 2026) by Christian Kümmerle and Dustin G. Mixon constructs explicit real m × n matrices with the restricted isometry property for sparsity k = m^(2/3−o(1)). Tao asked for such explicit constructions in 2007; elementary ones stop at exponent 1/2, and Bourgain et al. (2011) passed it only by a small ε. The authors state that "Theorem 1 was proved in one shot using GPT-6 Astra" and that the result is formalized in Lean; the paper is a preprint. ## 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 ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 194 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 133 days after its cutoff - Gemini 4 Hydrogen (training cutoff March 2026): 224 days after its cutoff - Grok 4.7 (training cutoff May 2026): 163 days after its cutoff ## Sources 1. [arXiv 2611.14475: Explicit restricted isometries with k = m^(2/3−o(1)) (Kümmerle, Mixon)](https://arxiv.org/abs/2611.14475) (arxiv.org, paper) 2. [Dustin Mixon, Short, Fat Matrices: Explicit restricted isometries well beyond the square-root bottleneck (11 Nov)](https://dustingmixon.wordpress.com/2026/11/11/explicit-restricted-isometries-well-beyond-the-square-root-bottleneck/) (dustingmixon.wordpress.com, discussion) 3. [Terence Tao (2007): Open question: deterministic UUP matrices](https://terrytao.wordpress.com/2007/07/02/open-question-deterministic-uup-matrices/) (terrytao.wordpress.com, discussion) ## Changes - 2026-11-12 (filed): Created (science agent; arXiv PDF disclosure and Mixon's blog post read) ## Related - 2026-11-11: [AI-assisted results, 11 Nov: arXiv and Hexagon](https://postcutoff.com/e/2026-11-11-ai-assisted-results-november-11-listing/index.md) - People: [Terence Tao](https://postcutoff.com/person/terence-tao/)