An improved upper bound for the Chvátal–Sankoff constant

Take two random binary strings of length n. Their longest common subsequence, the longest string that appears in both in order, has length about γ₂·n. Chvátal and Sankoff proved in 1975 that this constant exists.¹ Its value is still unknown.

In August 2026 Reason and Sven Myhre proved γ₂ ≤ 0.824443, improving 0.826280, Lueker’s bound that had stood since 2009.² The proof is a finite certificate: 400,253,317 positive integers satisfying one inequality at every state of a finite automaton, checked in exact integer arithmetic. The code, certificate, verifier and paper are in the repository.³

It is no longer the best bound. In October two independent groups went further with the same method, to 0.824120 and then 0.821963.¹⁰¹¹

The problem

Let Lₙ be the length of the longest common subsequence of two independent, uniformly random binary strings of length n. Since E[Lₙ] is superadditive, Fekete’s lemma gives

$$\gamma_2 \;=\; \lim_{n\to\infty} \frac{\mathbb{E}[L_n]}{n} \;=\; \sup_{n\ge 1} \frac{\mathbb{E}[L_n]}{n}.$$

Simulations put γ₂ near 0.8122.⁴ Steele conjectured 2/(1+√2) ≈ 0.828427 in 1986.⁵ Lueker disproved that in 2009 by proving γ₂ ≤ 0.826280, refining the automaton method of Dančík and Paterson.⁶ The best lower bound is 0.792665992, from 2025.⁷

A 2018 dissertation reports 0.825101 but gives neither its parameters nor a certificate, so we treat it as a report.⁸ The new bound improves it by 0.000658 and Lueker’s by 0.001837.

Counting lists of matches

If two strings share a common subsequence of length m, they can be cut into m pieces that each end in a match. The smallest such pieces, minimal match pairs, are

$$T_{c,\ell} = \begin{cases} (\bar c^{\,\ell} c,\; c), & \ell \ge 0,\\ (c,\; \bar c^{\,-\ell} c), & \ell < 0, \end{cases} \qquad c \in \{0,1\},\quad \bar c = 1 - c,\quad \ell \in \mathbb{Z},$$

each with |ℓ| + 2 characters. Lueker proved that every string pair with LCS m comes from a canonical list of m such pairs plus a tail with no common character.² Bounding long common subsequences becomes counting long lists.

Counting every list is too generous, so an automaton filters them. It remembers the last h characters of each string and enough of the dynamic-programming table to reject lists that cannot be canonical, and it never rejects a canonical one. A larger h gives a tighter bound, and an automaton about eight times larger per step.

The automaton

A state is a four-tuple (x, y, dˣ, dʸ): the last h bits of each string and two 0–1 difference vectors along the table’s boundary, taken up to complementing every bit. At h = 10 there are 400,253,317 states.

Transitions are labelled by the appended pair, truncated to the history. The two boundary labels stand for every longer pair, summed as a geometric series. That gives 38 labels with weights

$$w_\ell(z) = \begin{cases} z^{|\ell|+2}, & |\ell| < h-1,\\[4pt] \dfrac{z^{h+1}}{1-z}, & |\ell| = h-1, \end{cases}$$

and, for 0 < z < 1/2, the operator

$$(A v)(q) \;=\; \sum_{(c,\ell)\,:\,\delta(q,c,\ell) \neq \varnothing} w_\ell(z)\, v\bigl(\delta(q,c,\ell)\bigr).$$

Lueker’s criterion: if a positive v and 0 < λ < 1 satisfy Av ≤ λv in every coordinate, the weighted count of accepted lists of m pairs decays like λᵐ.² Compared with the 4ⁿ string pairs, up to polynomial factors,

$$\Pr\bigl[L_n \ge \gamma n\bigr] \;\lesssim\; \lambda^{\gamma n}\,(2z)^{-2n},$$

which vanishes once γ log λ < 2 log(2z). Hence

$$\gamma_2 \;\le\; \frac{2 \log(2z)}{\log \lambda}.$$

The theorem is Lueker’s. The new work adds no new mathematics: it takes his calculation from h = 8 to h = 10 and makes it fit, and check exactly, on one desktop computer.

The certificate

The certificate fixes z = 3209/10000 and rounds every weight up to an integer:

$$W_\ell = \bigl\lceil 2^{32}\, w_\ell(z) \bigr\rceil.$$

For a witness V of 400,253,317 positive integers, the verifier computes in 64-bit integers

$$S_q \;=\; \sum_{(c,\ell)\,:\,\delta(q,c,\ell) \neq \varnothing} W_\ell\, V_{\delta(q,c,\ell)} \qquad\text{and checks}\qquad S_q \;\le\; \Lambda\, V_q$$

with Λ = 1,464,651,560. Rounding up only makes the check harder, so passing it proves Av ≤ λv for λ = Λ/2³².

The last step avoids floating point. For positive integers p and q,

$$\frac{2\log(2z)}{\log\lambda} \le \frac{p}{q} \iff (2z)^{2q} \ge \lambda^{p}.$$

The verifier decides this for p/q = 824443/1000000 with rational bounds on both logarithms. It passes for 0.824443 and fails for 0.824442.

The witness came from 113 sweeps of floating-point power iteration. The search is not part of the proof: the stored integers either pass or fail.

What was verified

The verifier authenticates the automaton and the witness by SHA-256, checks positivity and closure, tests all 400,253,317 inequalities in integers, and decides the final bound in exact rationals. A full replay takes about 90 minutes on an 18-core desktop with 64 GB of memory.

Three controls show the checker can fail. The same witness does not prove 0.824442. At h = 8 the pipeline certifies Lueker’s 0.826280 and nothing better. A witness with one corrupted entry is rejected.

The certificate is only as good as the automaton. The dangerous bug is a transition wrongly marked as rejecting, which would make the bound look better than it is. An independent Python implementation of Lueker’s transition rule agrees with the C builder on every transition for h = 2 to 6, and on 760,000 sampled transitions at h = 10.

The builder also reproduces Lueker’s published Table II for h = 2 to 8: the exact number of states, and every bound to all six printed decimals.²

Since August

In October 2026 Leandre Jack ran the same h = 10 automaton, with the same 400,253,317 states, at z = 0.3376 and proved γ₂ ≤ 0.824120.¹⁰ Our z = 3209/10000 was not optimized, and the repository never claimed it was.

Later in October Tejasvi Singh Tomar carried Lueker’s method to h = 13 and proved γ₂ ≤ 0.821963. The bounds for h = 9 to 12 are checked by the Lean proof assistant’s kernel.¹¹

Both are independent computations, and both corroborate this one: they find the same automaton at h = 10, and their smaller certified bounds imply ours. None of the three has been peer reviewed, so Lueker’s 0.826280 is still the best refereed upper bound.

Limitations

The automaton is evidenced, not proven Agreement with Lueker’s table and with the second implementation is strong evidence, not a formal proof. There is no Lean formalization yet.

The h = 10 cross-check is sampled It covers 760,000 of 15,209,626,046 transitions. A full check exists but has not been run.

How the work was done

Reason selected the problem, extracted the certificate condition from Lueker’s paper, wrote the builder, the search, the second implementation and the verifier, ran the certification and drafted the paper. Sven Myhre directed the work, set the verification standard, replayed the verifier independently and takes responsibility for the claim.³

The campaign began on the lower bound and found that one desktop could not reach the 2025 record. It turned to the upper bound, reproduced Lueker’s 0.826280 at h = 8 as a calibration gate, sized the largest automaton that fit in memory, and converged overnight. The session transcript is public.⁹

The discipline mattered more than the search: reproduce the record first, search in floating point, certify in integers, ship a verifier that can fail, and say what is unchecked.