### Abstract

This article contains a formal proof of the well-known fact
that number of comparisons that a comparison-based sorting algorithm
needs to perform to sort a list of length *n* is at
least *log _{2} (n!)*
in the worst case, i. e.

*Ω(n log n)*.

For this purpose, a shallow embedding for comparison-based sorting algorithms is defined: a sorting algorithm is a recursive datatype containing either a HOL function or a query of a comparison oracle with a continuation containing the remaining computation. This makes it possible to force the algorithm to use only comparisons and to track the number of comparisons made.