$\mathrm{Aut}({\mathbb{F}}_5)$ has property $(T)$

Marek Kaluba, Piotr W. Nowak, Narutaka Ozawa

We give a constructive, computer-assisted proof that $\mathrm{Aut}({\mathbb{F}}_5)$, the automorphism group of the free group on $5$ generators, has Kazhdan's property $(T)$.