Abstract: 
This article contains a formal proof of the wellknown fact
that number of comparisons that a comparisonbased 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 comparisonbased 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. 
BibTeX: 
@article{Comparison_Sort_Lower_BoundAFP,
author = {Manuel Eberl},
title = {Lower bound on comparisonbased sorting algorithms},
journal = {Archive of Formal Proofs},
month = mar,
year = 2017,
note = {\url{http://isaafp.org/entries/Comparison_Sort_Lower_Bound.shtml},
Formal proof development},
ISSN = {2150914x},
}
