Kazhdan's property (T) is a strong rigidity property for groups. In recent years a new method has been established for proving property (T) with the computer. We showed that the optimization problem at the heart of the computer proof satisfies strong duality and that the dual problem has a geometric interpretation similar to property (FH). Using this geometric picture we simplified the problem and proved property (T) for the group $Aut(F_4)$.