TejasviTomar
November 2026 · Preprint

Sorting networks on 15 and 16 inputs need 55 and 60 comparators, and 20 inputs need 81

Tejasvi Singh Tomar

Abstract

Let S(N) be the least number of comparators in a sorting network on N inputs. We prove that S(16) = 60, so the sorting network with 60 comparators that Green found in 1969 has the fewest possible comparators. We also prove that S(15) ≥ 55, which leaves 55 and 56 as the possible values of S(15), and that S(20) ≥ 81. Together, these results raise the previously known lower bounds on S(N) for 17 ≤ N ≤ 32 by two for even N ≥ 20 and by one otherwise. The lower bounds for 16 and 20 inputs come from a rigidity argument: in a sorting network with one comparator fewer than the bound to be proved, the lower bounds for fewer inputs, among them S(15) ≥ 55 at 16 inputs and S(16) ≥ 60 at 20 inputs, fix the comparators through which the two largest and the two smallest values pass, wherever they enter, up to an explicit list of choices, and a computation rules out each choice. At 20 inputs, fixing these comparators also needs a search over the ways in which the two largest values can pass through the network. The proof of S(15) ≥ 55 follows the method of our computer-assisted proof of S(14) ≥ 50 and adds new lower bounds of Huffman type on the number of comparators needed to sort a set of vectors. Separately written programs check the computations. In Lean 4 we prove one step of the argument for S(15) ≥ 55 and derive the three results, assuming only two tables of bounds from our proof of S(14) ≥ 50 that are certified outside Lean; some steps are evaluated by compiled code rather than by Lean's kernel.

In plain words

A sorting network puts numbers in order using a fixed sequence of compare-and-swap steps. Because the sequence never depends on the numbers, such networks are well suited to parallel sorting and to secure computation between several parties. In 1969 Green found a network that sorts 16 numbers in 60 steps, but no one could rule out a shorter one. This paper proves that none exists. It also shows that 15 numbers need at least 55 steps and 20 numbers at least 81. The best network known for 15 numbers uses 56.

Sixteen horizontal wires crossed by 60 vertical comparator bars in ten layers. Thick magenta lines run from the left end of every wire through black comparators in the first four layers to the bottom wire, labelled largest; thick blue lines run in the same way to the top wire, labelled smallest. The comparators of the last six layers are grey.
Illustration of Green’s 60-comparator, ten-layer sorting network on 16 inputs, as written in the paper’s Lean proofs. Each comparator, drawn as a vertical bar, compares the values on the two wires it joins and puts the larger on the lower wire. For each of the 16 inputs, the magenta lines trace the path the largest value would take from that input to the bottom wire, and the blue lines trace the path the smallest value would take to the top wire. The comparators on these paths are drawn in black. The largest and smallest values each meet exactly four comparators, one in each of the first four layers, whichever input they start from. The paper shows that if a sorting network on 16 inputs had only 59 comparators, the paths of its largest and smallest values would again meet exactly four comparators each. The lower bound of 50 comparators for 14 inputs then narrows the possible paths of the second-largest and second-smallest values to a list of candidates. A computation rules out every candidate, so no sorting network on 16 inputs has only 59 comparators.

Formal statement and axioms

Each main result as stated in Lean, copied verbatim from the published package, with the axioms that the proof rests on. Lean v4.35.0-rc3, Mathlib c55e6e786f49. The package.

Sortnet.S15.S15_ge_55_N

S(15) ≥ 55: with compiled code

theorem Sortnet.S15.S15_ge_55_N :
    Sortnet.S14.coreTableC.Valid →
    (∀ i ∈ Sortnet.S14.Wed.done, (Sortnet.S14.Wed.TLf i).Valid) →
    Sortnet.S15.S15Statement
Definitions used in the statement
def S15Statement : Prop := ∀ net : Network 15, net.Sorts → 55 ≤ net.length
structure Comparator (n : Nat) where
  i : Fin n
  j : Fin n
  lt : i < j
  deriving DecidableEq
def Comparator.apply {n : Nat} (c : Comparator n) (v : Fin n → Nat) : Fin n → Nat :=
  fun k => if k = c.i then min (v c.i) (v c.j) else if k = c.j then max (v c.i) (v c.j) else v k
abbrev Network (n : Nat) := List (Comparator n)
def Network.eval {n : Nat} (net : Network n) (v : Fin n → Nat) : Fin n → Nat :=
  net.foldl (fun w c => c.apply w) v
def Network.Sorts {n : Nat} (net : Network n) : Prop :=
  ∀ v : Fin n → Nat, ∀ a b : Fin n, a ≤ b → net.eval v a ≤ net.eval v b
def bitSet (n K : ℕ) : Set (Vec n) := {v | Nat.testBit K (code v) = true}
structure Table where
  cnt : ℕ
  ent : ℕ → ℕ × ℕ × ℕ
def Table.Valid (T : Table) : Prop :=
  ∀ i < T.cnt, ((T.ent i).1 = 10 ∨ (T.ent i).1 = 11) → LB (bitSet (T.ent i).1 (T.ent i).2.1) (T.ent i).2.2

Source: Zenodo record 24156534, lean_tools.tar.gz/lean_tools/assembly_n/S15AssemblyN.lean:45-48.

Axioms, as Lean reports them: propext, Classical.choice, Quot.sound and 269,587 more, for example Sortnet.certOK_harder11._native.native_decide.ax_1_1, Sortnet.S14.CSD.n_V2164_10._native.native_decide.ax_1_1 and Sortnet.S14.CSD.n_V2202_12._native.native_decide.ax_1_1. Each of these 269,587 axioms comes from a check that runs as compiled code (native_decide). The full report is recorded in zenodo:24156534/lean_tools.tar.gz/lean_tools/axioms/S15_ge_55_N.txt:1-269590.

Sortnet.S16.S16_eq_60_N

S(16) = 60: with compiled code

theorem Sortnet.S16.S16_eq_60_N :
    Sortnet.S14.coreTableC.Valid →
    (∀ i ∈ Sortnet.S14.Wed.done, (Sortnet.S14.Wed.TLf i).Valid) →
    Sortnet.S16.S16Statement ∧ ∃ net : Sortnet.Network 16, net.Sorts ∧ net.length = 60
Definitions used in the statement
def S16Statement : Prop := ∀ net : Network 16, net.Sorts → 60 ≤ net.length
structure Comparator (n : Nat) where
  i : Fin n
  j : Fin n
  lt : i < j
  deriving DecidableEq
def Comparator.apply {n : Nat} (c : Comparator n) (v : Fin n → Nat) : Fin n → Nat :=
  fun k => if k = c.i then min (v c.i) (v c.j) else if k = c.j then max (v c.i) (v c.j) else v k
abbrev Network (n : Nat) := List (Comparator n)
def Network.eval {n : Nat} (net : Network n) (v : Fin n → Nat) : Fin n → Nat :=
  net.foldl (fun w c => c.apply w) v
def Network.Sorts {n : Nat} (net : Network n) : Prop :=
  ∀ v : Fin n → Nat, ∀ a b : Fin n, a ≤ b → net.eval v a ≤ net.eval v b
def bitSet (n K : ℕ) : Set (Vec n) := {v | Nat.testBit K (code v) = true}
structure Table where
  cnt : ℕ
  ent : ℕ → ℕ × ℕ × ℕ
def Table.Valid (T : Table) : Prop :=
  ∀ i < T.cnt, ((T.ent i).1 = 10 ∨ (T.ent i).1 = 11) → LB (bitSet (T.ent i).1 (T.ent i).2.1) (T.ent i).2.2

Source: Zenodo record 24156534, lean_tools.tar.gz/lean_tools/assembly_n/S16EqAssemblyN.lean:70-73.

Axioms, as Lean reports them: propext, Classical.choice, Quot.sound and 269,608 more, for example Sortnet.certOK_harder11._native.native_decide.ax_1_1, Sortnet.S16.checkL1_ok._native.native_decide.ax_1_1 and Sortnet.S16.orbit0_ok._native.native_decide.ax_1_1. Each of these 269,608 axioms comes from a check that runs as compiled code (native_decide). The full report is recorded in zenodo:24156534/lean_tools.tar.gz/lean_tools/axioms/S16_eq_60_N.txt:1-269611.

Sortnet.S20.S20_ge_81_N

S(20) ≥ 81: with compiled code

theorem Sortnet.S20.S20_ge_81_N :
    Sortnet.S14.coreTableC.Valid →
    (∀ i ∈ Sortnet.S14.Wed.done, (Sortnet.S14.Wed.TLf i).Valid) →
    Sortnet.S20.S20Statement
Definitions used in the statement
def S20Statement : Prop := ∀ net : Network 20, net.Sorts → 81 ≤ net.length
structure Comparator (n : Nat) where
  i : Fin n
  j : Fin n
  lt : i < j
  deriving DecidableEq
def Comparator.apply {n : Nat} (c : Comparator n) (v : Fin n → Nat) : Fin n → Nat :=
  fun k => if k = c.i then min (v c.i) (v c.j) else if k = c.j then max (v c.i) (v c.j) else v k
abbrev Network (n : Nat) := List (Comparator n)
def Network.eval {n : Nat} (net : Network n) (v : Fin n → Nat) : Fin n → Nat :=
  net.foldl (fun w c => c.apply w) v
def Network.Sorts {n : Nat} (net : Network n) : Prop :=
  ∀ v : Fin n → Nat, ∀ a b : Fin n, a ≤ b → net.eval v a ≤ net.eval v b
def bitSet (n K : ℕ) : Set (Vec n) := {v | Nat.testBit K (code v) = true}
structure Table where
  cnt : ℕ
  ent : ℕ → ℕ × ℕ × ℕ
def Table.Valid (T : Table) : Prop :=
  ∀ i < T.cnt, ((T.ent i).1 = 10 ∨ (T.ent i).1 = 11) → LB (bitSet (T.ent i).1 (T.ent i).2.1) (T.ent i).2.2

Source: Zenodo record 24156534, lean_tools.tar.gz/lean_tools/assembly_n/S20AssemblyN.lean:71-74.

Axioms, as Lean reports them: propext, Classical.choice, Quot.sound and 269,641 more, for example Sortnet.certOK_harder11._native.native_decide.ax_1_1, Sortnet.S16.checkL1_ok._native.native_decide.ax_1_1 and Sortnet.S16.orbit0_ok._native.native_decide.ax_1_1. Each of these 269,641 axioms comes from a check that runs as compiled code (native_decide). The full report is recorded in zenodo:24156534/lean_tools.tar.gz/lean_tools/axioms/S20_ge_81_N.txt:1-269644.

2 more formal statements

Sortnet.T6.table6Lo_N

the paper’s lower bounds for 17 ≤ N ≤ 27: with compiled code

theorem Sortnet.T6.table6Lo_N :
    Sortnet.S14.coreTableC.Valid →
    (∀ i ∈ Sortnet.S14.Wed.done, (Sortnet.S14.Wed.TLf i).Valid) →
    Sortnet.T6.Table6Lo
Definitions used in the statement
def Table6Lo : Prop :=
  Sortnet.S20.S17Statement ∧ Sortnet.S20.S18Statement ∧ Sortnet.S20.S19Statement ∧ Sortnet.S20.S20Statement ∧
    S21Statement ∧ S22Statement ∧ S23Statement ∧ S24Statement ∧ S25Statement ∧ S26Statement ∧ S27Statement
def S17Statement : Prop := ∀ net : Network 17, net.Sorts → 65 ≤ net.length
def S18Statement : Prop := ∀ net : Network 18, net.Sorts → 70 ≤ net.length
def S19Statement : Prop := ∀ net : Network 19, net.Sorts → 75 ≤ net.length
def S20Statement : Prop := ∀ net : Network 20, net.Sorts → 81 ≤ net.length
def S21Statement : Prop := ∀ net : Network 21, net.Sorts → 86 ≤ net.length
def S22Statement : Prop := ∀ net : Network 22, net.Sorts → 92 ≤ net.length
def S23Statement : Prop := ∀ net : Network 23, net.Sorts → 97 ≤ net.length
def S24Statement : Prop := ∀ net : Network 24, net.Sorts → 103 ≤ net.length
def S25Statement : Prop := ∀ net : Network 25, net.Sorts → 108 ≤ net.length
def S26Statement : Prop := ∀ net : Network 26, net.Sorts → 114 ≤ net.length
def S27Statement : Prop := ∀ net : Network 27, net.Sorts → 119 ≤ net.length
structure Comparator (n : Nat) where
  i : Fin n
  j : Fin n
  lt : i < j
  deriving DecidableEq
def Comparator.apply {n : Nat} (c : Comparator n) (v : Fin n → Nat) : Fin n → Nat :=
  fun k => if k = c.i then min (v c.i) (v c.j) else if k = c.j then max (v c.i) (v c.j) else v k
abbrev Network (n : Nat) := List (Comparator n)
def Network.eval {n : Nat} (net : Network n) (v : Fin n → Nat) : Fin n → Nat :=
  net.foldl (fun w c => c.apply w) v
def Network.Sorts {n : Nat} (net : Network n) : Prop :=
  ∀ v : Fin n → Nat, ∀ a b : Fin n, a ≤ b → net.eval v a ≤ net.eval v b
def bitSet (n K : ℕ) : Set (Vec n) := {v | Nat.testBit K (code v) = true}
structure Table where
  cnt : ℕ
  ent : ℕ → ℕ × ℕ × ℕ
def Table.Valid (T : Table) : Prop :=
  ∀ i < T.cnt, ((T.ent i).1 = 10 ∨ (T.ent i).1 = 11) → LB (bitSet (T.ent i).1 (T.ent i).2.1) (T.ent i).2.2

Source: Zenodo record 24156534, lean_tools.tar.gz/lean_tools/assembly_n/T6AssemblyN.lean:70-73.

Axioms, as Lean reports them: propext, Classical.choice, Quot.sound and 269,644 more, for example Sortnet.certOK_harder11._native.native_decide.ax_1_1, Sortnet.S16.checkL1_ok._native.native_decide.ax_1_1 and Sortnet.S16.orbit0_ok._native.native_decide.ax_1_1. Each of these 269,644 axioms comes from a check that runs as compiled code (native_decide). The full report is recorded in zenodo:24156534/lean_tools.tar.gz/lean_tools/axioms/table6Lo_N.txt:1-269647.

Sortnet.S16.green_sorts

kernel-only for the proof that Green’s network sorts

theorem green_sorts : greenNet.Sorts
Definitions used in the statement
def greenNet : Network 16 :=
  [gc 0 1, gc 2 3, gc 4 5, gc 6 7, gc 8 9, gc 10 11, gc 12 13, gc 14 15,
   gc 0 2, gc 1 3, gc 4 6, gc 5 7, gc 8 10, gc 9 11, gc 12 14, gc 13 15,
   gc 0 4, gc 1 5, gc 2 6, gc 3 7, gc 8 12, gc 9 13, gc 10 14, gc 11 15,
   gc 0 8, gc 1 9, gc 2 10, gc 3 11, gc 4 12, gc 5 13, gc 6 14, gc 7 15,
   gc 5 10, gc 6 9, gc 3 12, gc 13 14, gc 7 11, gc 1 2, gc 4 8,
   gc 1 4, gc 7 13, gc 2 8, gc 11 14, gc 5 6, gc 9 10,
   gc 2 4, gc 11 13, gc 3 8, gc 7 12,
   gc 6 8, gc 10 12, gc 3 5, gc 7 9,
   gc 3 4, gc 5 6, gc 7 8, gc 9 10, gc 11 12,
   gc 6 7, gc 8 9]
def gc (i j : Fin 16) (h : i < j := by decide) : Comparator 16 := ⟨i, j, h⟩
structure Comparator (n : Nat) where
  i : Fin n
  j : Fin n
  lt : i < j
  deriving DecidableEq
def Comparator.apply {n : Nat} (c : Comparator n) (v : Fin n → Nat) : Fin n → Nat :=
  fun k => if k = c.i then min (v c.i) (v c.j) else if k = c.j then max (v c.i) (v c.j) else v k
abbrev Network (n : Nat) := List (Comparator n)
def Network.eval {n : Nat} (net : Network n) (v : Fin n → Nat) : Fin n → Nat :=
  net.foldl (fun w c => c.apply w) v
def Network.Sorts {n : Nat} (net : Network n) : Prop :=
  ∀ v : Fin n → Nat, ∀ a b : Fin n, a ≤ b → net.eval v a ≤ net.eval v b

Source: Zenodo record 24156534, lean_src.tar.gz/lean_src/S16/Green.lean:112.

Axioms, as Lean reports them.

'Sortnet.S16.green_sorts' depends on axioms: [propext, Classical.choice, Quot.sound]