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, 26/26).
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. The proof lives at research/sorting-networks/lean/ZeroOnePrinciple.lean — the Wasteland's first machine-checked stratum (the verification is the artifact).
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). 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