A sorting network is a machine with no branches and no memory — just a fixed list of compare-and-swap wires. It must put every possible input in order. For n things that is n! orderings: for sixteen inputs, twenty trillion of them. Yet you never have to check more than the 2n inputs made only of zeros and ones. Pass those, and you have sorted everything. This page lets you wire the machine, break it, and watch the certificate catch the lie.
Here is a strange kind of machine. It sorts numbers, but it cannot look at them. A normal sorting program asks questions — is this bigger than that? — and decides what to do next based on the answer. A sorting network asks the same question at the same wires no matter what the answer is. Its entire program is fixed before it ever sees a number: a list of comparators, each one a little gate straddling two wires that compares the two values passing through and, if they're out of order, swaps them. Same gates, same order, every time. This obliviousness is exactly why hardware loves them — a sorting network is a circuit, etched once, that sorts at the speed of its wires.
But it raises a sharp problem. If the machine can't adapt, how do you ever know it's right — that it sorts not just the inputs you tried, but all of them? A list of comparators that looks plausible can fail on one obscure arrangement out of millions. You could test all n! permutations, but that number runs away from you fast. The answer — a classical theorem, developed in Knuth's Art of Computer Programming1 — is one of the cleanest in computing, and it is the reason this whole page can tell the truth cheaply:
The zero-one principle.
A comparator network sorts every input
if and only if it sorts every input made of 0s and 1s.
So to vouch for all n! orderings, test the 2n binary strings. Nothing more.
Below is a sorting network drawn the way they always are: n horizontal wires carrying values left to right, and the comparators as vertical rungs. Each rung compares its two wires and puts the smaller value on the upper wire. The network shown is Batcher's odd–even mergesort2 — a real, named construction from 1968 that works for any n. Feed it a scrambled input and watch the values fall into order, one column at a time. Click any rung to disable it — break the machine on purpose — and the rest of the page will react.
One successful run proves nothing — the machine could still choke on some input you didn't try. So here is the real test, run in full. The page takes the network above and pushes all 2n strings of zeros and ones through it. If every one comes out sorted (all the 0s, then all the 1s), the zero-one principle promises that all n! real orderings sort too — and the machine is certified. Disable a rung in panel 1 and watch the certificate find the exact binary strings the broken machine now leaves out of order.
It feels like a cheat. Real inputs have endless distinct values; how can two symbols stand in for all of them? The reason is that a comparator is monotone. Take any rung, feed it two values, and apply some increasing relabelling f to everything — squaring, shifting, or the harshest relabelling of all, rounding everything below a threshold to 0 and everything at-or-above to 1. The rung does the same thing either way: it commutes with f. Lift that over the whole network and you get one clean identity — NET(f(x)) = f(NET(x)) — which says you can squash first or sort first, the result is the same.
So suppose a network fails to sort some real input x: somewhere in its output a bigger value sits above a smaller one. Pick the threshold right between them. Squashing x turns it into a string of 0s and 1s — and because squash-then-sort equals sort-then-squash, that binary string comes out with a 1 stranded above a 0. The failure survives the squash. Every real failure casts a binary shadow; check the shadows and you've checked everything. Drag the threshold and watch a real failure collapse onto its binary witness:
Once you can certify a network cheaply, a sharper question opens: what is the smallest machine that sorts n things — fewest comparators (its size), or fewest parallel columns (its depth, the time a hardware sorter takes)? Batcher's construction is simple and regular, and for small n it is already as good as possible. But it is not magic: past a point it spends rungs it doesn't need. The table compares Batcher's machine — size and depth recomputed live — against the values that have been proven minimal.3
Green = Batcher meets the proven minimum; red = it overspends. Proven optima are cited, not recomputed here — only Batcher's own numbers are. The minimum size is settled only up to n = 12; the minimum depth only up to n = 17. Beyond that, the smallest sorting network for even modest n is an open problem — every value past those lines is a current record, not a proof. (Asymptotically, the AKS network4 reaches the theoretically optimal O(n log n) size and O(log n) depth, but its hidden constants are so vast it has never beaten Batcher at any size anyone would build.)
Everything above is recomputed in your browser, now, from the same code that draws it. This strip re-runs the load-bearing claims against fresh random networks each time you reload — the same checks the offline verifier makes (research/sorting-networks/verify.mjs, 41/41).
Everything above checks the zero-one principle; none of it proves it. Section 5 can only sample — fresh random networks, a finite n — and no finite test can ever settle a claim about every network of every width. That last gap is the one thing a running page cannot close by itself. So we closed it the only honest way: a proof a machine has checked.
The zero-one principle is now a theorem in Lean 4, certified by the proof assistant's kernel. The file imports nothing — not even a standard library — so the only thing trusted is Lean's type checker itself; every order law it uses (reflexivity, transitivity, totality) is proved from scratch inside it.
theorem zero_one [Ord' α] (net : List (Fin n × Fin n))
(H : ∀ w : Fin n → Bool, Sorted (run net w)) :
∀ v : Fin n → α, Sorted (run net v)
For any comparator network net on n wires: if it sorts every Bool (0/1) input, then it sorts every input over any total order. The whole proof turns on one lemma — a comparator commutes with the monotone threshold x ↦ (a ≤ x) — which is exactly the monotone identity NET(f(x)) = f(NET(x)) the "binary shadow" instrument in §3 lets you watch by hand.
Reproduce it from a bare checkout: bash research/sorting-networks/lean/install-lean.sh && bash research/sorting-networks/lean/verify.sh (or, where GitHub release egress is blocked, the github-free install-lean-nix.sh). The proof lives at research/sorting-networks/lean/ZeroOnePrinciple.lean — the Wasteland's first machine-checked stratum (the verification is the artifact).
§6 proves the law. This is the law spent. The same Lean file now hands its kernel three concrete, size-optimal networks — the very ones you can dial up in panel 1 (n = 4, 5, 8) — makes the kernel run the 2n zeros-and-ones test itself, and then invokes the proven principle to conclude each one sorts every input over any total order. The inference the whole page is about — check the 2n binary strings, conclude all n! orderings — is now performed end to end by a proof assistant, for real machines, not sampled.
Watch the counting gap close in one line. For the eight-wire network, "sorts correctly" naively means sorts all 8! = 40 320 orderings. The kernel never enumerates them. It settles sorts all 28 = 256 Boolean inputs — and zero_one does the rest, vouching not just for those 40 320 orderings but for every input over the reals, the strings, any order at all.
def net8 : List (Fin 8 × Fin 8) := -- Batcher, 19 comparators = the proven minimum s(8) [(0,1),(2,3),(4,5),(6,7),(0,2),(1,3),(4,6),(5,7),(1,2),(5,6), (0,4),(1,5),(2,6),(3,7),(2,4),(3,5),(1,2),(3,4),(5,6)] theorem net8_sorts_bool : ∀ w : Fin 8 → Bool, Sorted (run net8 w) := by decide -- the kernel runs all 256 cases theorem net8_sorts [Ord' α] : ∀ v : Fin 8 → α, Sorted (run net8 v) := zero_one net8 net8_sorts_bool -- …lifted to every input, every order
| network | comparators | proven min s(n) | Bool inputs the kernel checks | orderings it thereby vouches for | verdict |
|---|---|---|---|---|---|
| net4 | 5 | 5 ✓ | 2⁴ = 16 | 4! = 24 | sorts all — kernel-checked |
| net5 | 9 | 9 ✓ | 2⁵ = 32 | 5! = 120 | sorts all — kernel-checked |
| net8 | 19 | 19 ✓ | 2⁸ = 256 | 8! = 40,320 | sorts all — kernel-checked |
Each network's comparator count is the smallest possible for its width — the proven minima s(4)=5, s(5)=9, s(8)=19 (Knuth). That minimality is cited, not reproven; what the kernel certifies is the other half — that these particular networks actually sort. Correctness machine-checked; optimality quoted. The two are kept apart on purpose.
And the certificate has teeth. Delete net4's last comparator and Lean proves — again by exhausting the 16 Boolean inputs — that it is no longer a sorter (theorem net4bad_not_sorter): the broken machine botches the input (1,0,1,0), handing back (0,1,0,1). The check that certifies is the same check that catches — exactly the break-a-rung game of panels 1–2, now settled by the kernel rather than by sampling.
All three certificates plus the negative live in the same zero-import file: research/sorting-networks/lean/ZeroOnePrinciple.lean; verify.mjs §F recomputes the identical comparator lists (and, if lean is on PATH, typechecks the proof live) so the browser check and the machine proof cannot drift apart.
Proved here, live. That a given network sorts is checked exhaustively over all 2n binary inputs. The zero-one principle's engine — the monotone identity NET(f(x)) = f(NET(x)) — is verified on thousands of (network, relabelling, input) triples, and the principle's verdict (binary test) is confirmed to agree with the brute-force permutation test on every random network up to n=7, where n! is still enumerable. Batcher's networks are generated and their sizes and depths recomputed.
Now proved here, for all cases. The zero-one principle itself — the universal statement no finite test above can reach — is machine-checked in Lean 4 (§6): a kernel-certified proof for every network and every width, importing no library and resting on axioms propext and Quot.sound alone (no sorry, no choice). And the principle is then spent (§7): the kernel runs the 2n test on three concrete size-optimal networks (n = 4, 5, 8) and, via zero_one, certifies each sorts every input over any order — a broken variant proved not to sort, all in the same zero-import file. Source + one-command reproduce in research/sorting-networks/lean/.
Cited, not reproven. Batcher's construction is classical (Batcher 1968); the principle is classical too (Knuth) but is now proved here, not merely cited. Theminimality of a size or depth — that no smaller network exists — is never something this page checks; those are hard computer-assisted theorems: sizes through n=8 classical, n=9,10 by Codish, Cruz-Filipe, Frank & Schneider-Kamp (2014), n=11,12 by Harder (2020); depths through n=10 classical, 11–16 by Bundala & Závodný (2014), n=17 by Ehlers & Müller. The convention here puts the smaller value on the upper wire; the mirror convention is equally common.
Choices. "Real-valued" inputs use distinct integers, which loses nothing — a comparator only ever consults the order of two values, never their size. The certificate's grid is shown in full only for small n; for larger n the count is exact but only the failures are listed.
1. D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, §5.3.4 ("Networks for Sorting"), where the zero-one principle and these networks are developed.
2. K. E. Batcher, "Sorting networks and their applications," AFIPS Spring Joint Computer Conference, 1968, pp. 307–314.
3. M. Codish, L. Cruz-Filipe, M. Frank, P. Schneider-Kamp, "Twenty-Five Comparators is Optimal when Sorting Nine Inputs (and Twenty-Nine for Ten)," ICTAI 2014. J. Harder, "An Answer to the Bose–Nelson Sorting Problem for 11 and 12 Channels," arXiv:2012.04400 (2020). D. Bundala, J. Závodný, "Optimal-Depth Sorting Networks," arXiv:1412.5302 (2014). T. Ehlers, M. Müller, "Faster Sorting Networks for 17, 19 and 20 Inputs," arXiv:1410.2736.
4. M. Ajtai, J. Komlós, E. Szemerédi, "An O(n log n) sorting network," STOC 1983 — optimal in asymptotic order, famously impractical in constant.
← back to the Wasteland