# Sixteen words cover all 15-bit strings

Partial progress on an open problem. Vamshi Jandhyala.

> Deleting five bits from every 15-bit string can leave just 16 different strings, down from 17 in 2013, so the growth rate of the n/3-deletion problem is at most 16^(1/15) < 1.2031; among symmetric sets 16 is optimal.

Canonical: https://vamshij.com/research/sixteen-words
Code and Lean proofs: https://github.com/jvvk/mathematics/tree/main/sixteen-words
Paper (PDF): https://github.com/jvvk/mathematics/blob/main/sixteen-words/paper/note.pdf

From every binary string of length `n = 3k` delete `k` bits, choosing the deletions so that as few distinct strings of length `2k` remain as possible ([MathOverflow 142857](https://mathoverflow.net/q/142857), 2013). The least number `H(3k, k)` grows like `α^(3k)`; the 2013 discussion showed `α` exists (blocks and Fekete's lemma), bounded it below by `2^(5/3)/3 ≈ 1.058`, and above by small covers, the best being a 17-word cover for `n = 15`: `α ≤ 17^(1/15) ≈ 1.2079`.

**Theorem.** These sixteen strings of length 10 cover length 15 (every 15-bit string contains one as a subsequence), and none can be dropped:

```
0000000000 0000000011 0000111110 0011001100 0011111111 0110000110 0110101001 0111110000
1000001111 1001010110 1001111001 1100000000 1100110011 1111000001 1111111100 1111111111
```

So `H(15,5) ≤ 16` and `α ≤ 16^(1/15) < 1.2031`. The set is closed under complement and reversal, and **no such symmetric set of 15 or fewer strings covers length 15**: found by CP-SAT, confirmed by Glucose on an independent encoding, whose DRAT proof of unsatisfiability is checked by drat-trim. Whether an asymmetric 15-word cover exists is open.

Preprint v1, 10 October 2026, not peer reviewed and not yet independently reviewed. The block argument, the submultiplicativity of `H`, Fekete's limit and the bound on `α` from a 16-word cover are formally verified in Lean 4 (`lean/`, standard axioms only); the cover itself and the symmetric optimum are finite computations checked by independent programs and a proof checker. The author used AI tools (Claude, Anthropic) in this work, as described in the paper's acknowledgement, and is responsible for its content.