Computer proofs for Property (T), and SDP duality

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. I will explain this approach from the perspective of the corresponding dual optimization problem, which has a geometric interpretation in terms of harmonic cocycles. This viewpoint can be used to simplify the computer calculation, making it feasible to prove Property (T) for $Aut(F_4)$.