  We show that 11-channel sorting networks have at least 35 comparators and
that 12-channel sorting networks have at least 39 comparators. This positively
settles the optimality of the corresponding sorting networks given in The Art
of Computer Programming vol. 3 and closes the two smallest open instances of
the Bose-Nelson sorting problem. We obtain these bounds by generalizing a
result of Van Voorhis from sorting networks to a more general class of
comparator networks. From this we derive a dynamic programming algorithm that
computes the optimal size for a sorting network with a given number of
channels. From an execution of this algorithm we construct a certificate
containing a derivation of the corresponding lower size bound, which we check
using a program formally verified using the Isabelle/HOL proof assistant.
