Li, Li & Liu: external-memory integer sorting beats the comparison bound, answering Aggarwal–Vitter (1988) by way of network coding, with ChatGPT/Codex and Lean
Awaiting review
Importance: major (4 of 5)The takeaway
A week after the Li–Li network coding conjecture fell, two of its authors turned the refutation into an algorithm: a deterministic external-memory sort of Θ(log N)-bit integers that uses asymptotically fewer block transfers than any comparison sort in some parameter ranges. ChatGPT and Codex ‘materially affected’ the constructions and analyses.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 15 October 2026
Your AI and this story
- GPT-6 Astra167 days after its cutoff
- Claude Opus 5.5106 days after its cutoff
- Gemini 4 Argon197 days after its cutoff
- Grok 4.7136 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 106 days before it.
Key facts
- Paper: ‘Undirected Network Coding and Faster External-Memory Integer Sorting’, arXiv 2610.20079 (cs.DS, 14 Oct 2026)
- Bound: for N integers of Θ(log N) bits, memory M words, block size B with 2B ≤ M ≤ N: O((N/B)·(1 + log N / ((log(M/B))^{1−ε}(log M)^ε))) transfers, ε > 0 an absolute constant; the comparison bound is Θ((N/B)(1 + log(N/M)/log(M/B))) [Aggarwal–Vitter 1988]
- Context: Farhadi, Hajiaghayi, Larsen and Shi (2019) showed that if the Li–Li conjecture held, no algorithm could beat comparison sorting in ranges including B ≥ log N. The conjecture was refuted on 7 Oct by Braverman–He and by Zhang–Li–Li; this paper notes that ‘invalidating the assumption behind a conditional lower bound does not itself produce a faster algorithm’ and supplies one
- Builds on OpenAI’s integer-multiplication work (‘[Ope26]’), whose recursive linear-circuit construction is adapted to block transfers
- Lean: ‘We also use Lean 4 to verify the sorting algorithm’s correctness and complexity bounds, and the strict advantage of coding over routing’ (github.com/rtyu-1/coded-sorting-lean)
- AI methodology (verbatim): ‘We used OpenAI’s ChatGPT, including Codex, to assist with exploring network-coding constructions and sorting algorithms, developing and examining mathematical arguments, implementing and debugging Lean proofs … The tools materially affected the constructions and algorithmic analyses in Sections 4–7’
What happened
In 2004 Zongpeng Li and Baochun Li conjectured that in undirected multiple-unicast networks network coding does no better than fractional routing. The conjecture mattered beyond networking: Farhadi, Hajiaghayi, Larsen and Shi showed in 2019 that it would rule out integer sorting faster than comparison sorting in external memory, which would close a question Aggarwal and Vitter asked in 1988. On 7 Oct 2026 the conjecture was refuted twice, both times with GPT-6 help (entry).
A week later Baochun Li, Zongpeng Li and Sirui Liu turned the refutation into an algorithm (arXiv 2610.200791). They build a coding counterexample suited to “address-field interchange”, rearrange data with recursive XOR circuits adapted from OpenAI’s integer-multiplication construction, and combine this with Columnsort and most-significant-digit radix partitioning. The result is a deterministic sort whose I/O count is asymptotically below the comparison bound in a range of parameters. The algorithm’s correctness and complexity bounds, and the advantage of coding over routing, are checked in Lean 4.
AI methodology section (verbatim): “We used OpenAI’s ChatGPT, including Codex, to assist with exploring network-coding constructions and sorting algorithms, developing and examining mathematical arguments, implementing and debugging Lean proofs, and preparing the manuscript and literature discussion. The tools materially affected the constructions and algorithmic analyses in Sections 4–7, the supporting arguments and formalization in Appendices A–D, and their exposition in Sections 1–3.”
No Hacker News thread was found on 15 Oct (Algolia). X was not searched directly.
Why it matters
It is a clear chain in which one AI-assisted refutation led to an AI-assisted algorithm: a disproved conjecture removed a conditional lower bound, and within a week the conjecture’s own authors used it to answer a 38-year-old question. External-memory integer sorting is a central problem of I/O-efficient algorithms. The gain is asymptotic and holds only in some parameter ranges, so its practical impact is not claimed.
What is disputed or not yet verified
| Verification | Lean 4 formalization of the algorithm’s correctness and complexity bounds (scope in Appendix D); unrefereed preprint |
|---|
Sources
2 sources from 2 sites. Numbers match the chips in the text.
2 sources: 2 primary
Primary
- arXiv 2610.20079: Undirected Network Coding and Faster External-Memory Integer Sortingarxiv.org, paper
- GitHub: rtyu-1/coded-sorting-leangithub.com, code
Changes
- Filed from the arXiv PDF