The solution to Kadison's problem on orthonormal bases of unitaries for type $\mathrm{II}_1$ factors

In 1967, Kadison asked whether every type $\mathrm{II}_1$ factor admits an orthonormal basis, with respect to its trace, consisting of unitaries. We resolve this problem in full generality and, more broadly, characterize the diffuse finite von Neumann algebras admitting such bases consisting of symmetries. Let $M$ be a diffuse finite von Neumann algebra with a faithful normal tracial state $τ$, let $κ$ be the density character of $L^2(M,τ)$, and identify $M$ with its canonical image in $L^2(M,τ)$. We prove that there exists a family $B\subset {s\in M:s=s^*=s^{-1},\ τ(s)=0}$ such that ${1}\cup B$ is an orthonormal basis of $L^2(M,τ)$ if and only if the density character of $L^2(zM,τ(z)^{-1}τ|_{zM})$ equals $κ$ for every nonzero central projection $z\in Z(M)$. In particular, every type $\mathrm{II}_1$ factor admits an orthonormal basis consisting of unitaries, thereby answering Kadison's question affirmatively. We also provide a Lean 4 formalization of the main results.