The Hunter–Raudvere bound

For every n ≥ 3, S(n) \ge n! + (n-1)! + (n-2)! + n - 3 + \frac{(n-2)! - (n-2)}{n^2 - 3n + 1}

Holds for: n ≥ 3
Announced: Jul 28, 2026
Proof: Lean proof
Coefficient of (n−3)!: 0

By Zach Hunter and Uku Raudvere.

Values

n	At least
3	9
4	33
5	153
6	869
7	5,888
8	46,103
9	408,338
10	4,032,575
11	43,912,566
12	522,580,501
13	6,746,243,919
14	93,887,403,944

Evidence

Lean proof, statement reviewed github.com/urdvr/superpermutations-hunter Commit d45222190031d162feb1f6f3cf5fe2d11fab726d Lean 4 formalization and paper 'A New Lower Bound for Superpermutations' by Zach Hunter and Uku Raudvere; no native_decide

Historical proof checks

These checks cover the bound’s mathematical statement. The paper and source notes are for citation.

statement reviewed

∀ n : ℕ, 3 ≤ n → ∀ w : Almanac.Word n, Almanac.IsSuperpermutation n w → (n.factorial : ℝ) + ((n-1).factorial : ℝ) + ((n-2).factorial : ℝ) + (n : ℝ) - 3 + (((n-2).factorial : ℝ) - ((n : ℝ)-2)) / ((n : ℝ)^2 - 3*(n : ℝ) + 1) ≤ (w.length : ℝ)

Original job: historical-20261024-145632-264cc426-hunter-pointwise. Original policy: 900414d5499e49fa450a3d19e46083d07c10a485ebbccaf2762c9866715669e4.

Linking lemma written by the Almanac.