HEXAGONbeta

Sorting networks on 13 inputs need 45 comparators

A mix of human-written and AI-generated textHuman understanding: all partscs.DS — Data Structures and Algorithmsmath.CO — Combinatorics

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Oct 26, 2026 / CC BY 4.0

Abstract

Let S(N)S(N) be the least number of comparators in a sorting network on NN inputs (the Bose--Nelson problem). The values are known for N≤12N\le12, and for 1313 inputs the smallest known sorting network, found by Juill\'e, has 4545 comparators. We prove S(13)≥45S(13)\ge45, so S(13)=45S(13)=45. Deleting the comparators met by the largest and the second largest input leaves a sorting network on N−2N-2 inputs, so S(N)≥S(N−2)+P(2,N)S(N)\ge S(N-2)+P(2,N), where P(2,N)P(2,N) is the least possible worst-case number of comparators met by these two values. Van Voorhis stated P(2,N)≥⌈lg⁡F(N)⌉P(2,N)\ge\lceil\lg F(N)\rceil for an explicit function FF, but Mericanii showed that his proof is invalid. We prove P(2,N)=⌈lg⁡F(N)⌉P(2,N)=\lceil\lg F(N)\rceil for 3≤N≤323\le N\le32 by a finite search, which rests on the structure of the tree of paths of the largest value, the comparators on these paths, and a forest of comparators that carries the second largest value. With S(11)=35S(11)=35 this bound gives only S(13)≥44S(13)\ge44. For 4545 we apply it to the suffix of a network: if a network with LL comparators sorts a set XX of 00-11 vectors, then for suitable pairs of inputs the two values meet at most L−cL-c comparators, where cc is the cost of sorting the residual set left when their paths are deleted. A breadth-first search over the sets produced by prefixes of a hypothetical sorting network with 4444 comparators discards each set for which no single network stays within all these budgets, and no set survives at depth 2525. A separate verifier checks the certificate written by the search. Two proofs in Lean 4 check the same certificate, and in one of them Lean's kernel checks every computation, with only the standard axioms. Juill\'e's network is checked in the kernel as well. As a consequence, each of the twenty lower bounds on S(N)S(N) for 13≤N≤3213\le N\le32 that rested on Van Voorhis's inequality is proved and raised by one.

References

  1. R. C. Bose and R. J. Nelson, A sorting problem , J. ACM 9 (1962), no. 2, 282--296, doi:10.1145/321119.321126 (https://doi.org/10.1145/321119.321126).DOI
  2. M. Codish, L. Cruz-Filipe, M. Frank, and P. Schneider-Kamp, Sorting nine inputs requires twenty-five comparisons , J. Comput. System Sci. 82 (2016), no. 3, 551--563, doi:10.1016/j.jcss.2015.11.014 (https://doi.org/10.1016/j.jcss.2015.11.014).DOI
  3. B. Dobbelaere, Smallest and fastest sorting networks for a given number of inputs , web page, https://bertdobbelaere.github.io/sorting_networks.html, consulted 2026-10-18 (history entry of 2025-04-21).link
  4. R. W. Floyd and D. E. Knuth, The Bose--Nelson sorting problem , A Survey of Combinatorial Theory (J. N. Srivastava et al., eds.), North-Holland, Amsterdam, 1973, pp. 163--172, doi:10.1016/B978-0-7204-2262-7.50020-X (https://doi.org/10.1016/B978-0-7204-2262-7.50020-X).DOI
  5. J. Harder, Certificate of the minimal size of 11-channel sorting networks , Zenodo, 2019, dataset, doi:10.5281/zenodo.4108365 (https://doi.org/10.5281/zenodo.4108365).DOI
  6. J. Harder, An answer to the Bose--Nelson sorting problem for 11 and 12 channels , arXiv:2012.04400v3 [cs.DS], 2022.arXiv
  7. J. Harder, Lower size bounds for sorting networks , source code, 2020, https://github.com/jix/sortnetopt, commit 0b5d09c . The bound is defined as lower_size_bound in the file checker/ verified/ Sorting_Network_Bound.thy , and the correctness of the checking function is the lemma check_proof_get_bound_spec in checker/ verified/ Checker.thy .link
  8. Q. Huangfu and J. A. J. Hall, Parallelizing the dual revised simplex method , Math. Program. Comput. 10 (2018), no. 1, 119--142, doi:10.1007/s12532-017-0130-5 (https://doi.org/10.1007/s12532-017-0130-5).DOI
  9. H. Juillé, Evolution of non-deterministic incremental algorithms as a new approach for search in state spaces , Proceedings of the Sixth International Conference on Genetic Algorithms (L. J. Eshelman, ed.), Morgan Kaufmann, San Francisco, 1995, pp. 351--358.
  10. D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching , 2nd ed., Addison-Wesley, Reading, MA, 1998.
Show all 19 referencesShow fewer references
  1. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci., vol. 12699, Springer, 2021, pp. 625--635, doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  2. The mathlib Community, The Lean mathematical library , Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, pp. 367--381, doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI
  3. Mericanii, Twenty tabulated lower bounds for sorting networks rest on an invalid proof: an audit of Van Voorhis (1972), and a partial repair , draft, August 2026, https://mericanii.com/work/s13/paper-correction.pdf, consulted 2026-10-18.link
  4. T. S. Tomar, , GitHub repository, , commit .
  5. T. S. Tomar, Certificate and verifier for ``Sorting networks on 13 inputs need 45 comparators'' , Zenodo, 2026, doi: (https://doi.org/\suppdoi).link
  6. T. S. Tomar, Programs and logs for ``Sorting networks on 13 inputs need at least 44 comparators'' , Zenodo, 2026, doi: (https://doi.org/\supptwodoi).link
  7. T. S. Tomar, A kernel-checked Lean proof that sorting networks on 13 inputs need 45 comparators , Zenodo, 2026, doi: (https://doi.org/\kerneldoi).link
  8. D. C. Van Voorhis, An improved lower bound for sorting networks , IEEE Trans. Comput. C-21 (1972), no. 6, 612--613, doi:10.1109/TC.1972.5009021 (https://doi.org/10.1109/TC.1972.5009021).DOI
  9. D. C. Van Voorhis, Toward a lower bound for sorting networks , Complexity of Computer Computations (R. E. Miller and J. W. Thatcher, eds.), Plenum Press, New York, 1972, pp. 119--129, doi:10.1007/978-1-4684-2001-2_12 (https://doi.org/10.1007/978-1-4684-2001-2_12).DOI

Version history

  1. v1Submitted by Tejasvi Singh TomarInitial depositCurrentOct 26, 2026