Lower Size Bounds for Sorting Networks
I computed and formally verified the minimal number of required comparators in a sorting network with 11 and 12 inputs. This was an open problem. I’m currently writing a paper about this, and will add more information when this is completed. All the source code used, including a formal proof in Isabelle/HOL can be found at my sortnetopt GitHub project.