Recovery balance is preserved by duality
Conjecture 1 of Gruica, Bar-Lev, Ravagnani and Yaakobi asks whether a linear code is recovery balanced if and only if its orthogonal dual is recovery balanced. Here, encoded coordinates are read independently and uniformly with replacement; recovery balance means that the expected number of reads needed to recover a coordinate is the same for every coordinate.
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Coding theory; random access in DNA storage
- Posed by
- Gruica, Bar-Lev, Ravagnani and Yaakobi, A Combinatorial Perspective on Random Access Efficiency for DNA Storage: arXiv v1 §VII (Jan 2024), Conj. 1 in v2; IEEE Trans. Inf. Theory (2025).
- Year posed
- 2024
- Years open
- 2y
- Solved
- 2026-10-04
- Model
- OpenAI Codex (GPT-6 Astra)
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 6 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
More strongly, for every encoded coordinate of a linear code of length , where is the expected number of independent uniform reads with replacement needed to recover that coordinate. Consequently, the recovery profile is constant for exactly when it is constant for , proving the conjecture. The argument pairs complementary observation sets, writes expectations as weighted sums over sets, and uses equal complementary weights. A coordinate known to be zero has recovery time zero. The written note also handles the convention requiring one read for such a coordinate: balance equivalence remains valid, but the coordinatewise sum requires a correction. Nonuniform sampling is outside this identity.
What the AI did
OpenAI Codex (GPT-6 Astra) selected and investigated the conjecture, developed the complementary-recovery and sampling argument, wrote the mathematical proof, implemented the Lean formalization and evidence checker, and prepared the exposition. The human collaborator directed the research, questioned scope and interpretation, and reviewed the presentation. The Lean build and axiom checks ran in bounded Azure jobs. This disclosure does not claim an independent human proof audit.
Verification
Read by this site on 6 October 2026, not rebuilt. Fifteen Lean files with mathlib, Lean 4.34.0; no sorry, admit, axiom declarations, native_decide, opaque, unsafe or implemented_by. The headline theorem codeRecoveryBalanced_dual_iff holds over any field; codeDual is the actual orthogonal complement, recovery is proved equivalent to the paper's column-in-span condition, and the expected number of reads is the correct tail sum. The repository's axiom log lists only propext, Classical.choice and Quot.sound. At that review, only author-provided build logs were available. A separate exact-arithmetic check written here on 68 random codes over GF(2), GF(3) and GF(5) of length up to 7 confirmed a_i(C) + a_i(C^perp) = n in every case. No independent expert has audited the formal statement.
Author update: the linked public GitHub Actions run rebuilt all 13 positive modules from commit 80e4dbf, rejected 2 false controls, and printed the final theorem's axioms: propext, Classical.choice and Quot.sound. Permanent compiler records and source hashes are in the repository. This does not replace an independent expert audit.
Sources
Submitted by ZestyRaven517 on