\begin{abstract}
We describe a formalization of asymptotic $O$ notation using the Isabelle/HOL proof assistant.
\end{abstract}