Yury Kudryashov wrote a paper about the rotation number for the CICM 2021 conference on intelligent computer mathematics.

Rotation number is the key numerical invariant of an orientation preserving circle homeomorphism. Circle self-maps $f : S^1 → S^1$, $S^1 = ℝ/ℤ$, constitute an important class of dynamical systems. They appear in applications, e.g., as Poincaré maps of continuous flows on the $2$-torus. The simplest circle self-maps are pure rotations $x ↦ x + a$. It turns out that any circle homeomorphism f is semiconjugate to a pure rotation $x ↦ x + τ(f)$. The number $τ(f)$ is called the rotation number of $f$.

This paper describes the current state of an ongoing project with aim to formalize various facts about circle dynamics in Lean. Currently, the formalized material includes the definition and basic properties of the translation number of a lift of a circle homeomorphism to the real line. Yury Kudryashov also formalized a theorem by Étienne Ghys that gives a necessary and sufficient condition for two actions of a group on the circle by homeomorphism to be semiconjugate to each other.