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

TL;DR

This paper provides a constructive, computer-assisted proof demonstrating that the automorphism group of a free group on five generators possesses Kazhdan's property (T), a significant property in group theory.

Contribution

The paper introduces the first computer-assisted proof confirming that Aut(F_5) has property (T), advancing understanding of automorphism groups of free groups.

Findings

Aut(F_5) has Kazhdan's property (T)

The proof is constructive and computer-assisted

This establishes new cases of property (T) in automorphism groups

Abstract

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