Kazhdan’s property (T) for groups has a number of applications in pure and applied mathematics. I will report the recent development by several hands on the heavily computer assisted methods of proving property (T) (with math rigor), which eventually confirmed property (T) for $\operatorname{Aut}(F_n)$, $n>3$, thus solving a well-known problem in geometric group theory. I then talk about my recent human effort in coping with the computer assisted proof.