I think it is appropriate to let MO users know (the OP himself knows it well) that this question was recently solved: **it is feasible** to provide a computer based proof for property (T) using the Ozawa Equation and this method was applied successfully to the groups mentioned in the question. In particular, the famous open problem alluded to above is now solved. The computation is done via [semidefinite programming][5], as suggested by David Speyer in his [answer][6]. See [Kaluba-Kielak-Nowak][1] for a proof that $\mathrm{Aut}(F_n)$ has (T) for $n\geq 5$. The case $n=5$ was treated earlier in [Kaluba-Nowak-Ozawa][2]. Some earlier positive results were obtained in [Netzer-Thom][4] and [Fujiwara-Kabaya][3]. We note that $\mathrm{Aut}(F_2)$ and $\mathrm{Aut}(F_3)$ are known not to have (T), and the case for $\mathrm{Aut}(F_4)$ is still open. This is all quite remarkable. [1]: https://arxiv.org/abs/1812.03456 [2]: https://arxiv.org/abs/1712.07167 [3]: https://arxiv.org/abs/1703.04555 [4]: https://arxiv.org/abs/1411.2488 [5]: http://en.wikipedia.org/wiki/Semidefinite_programming [6]: https://mathoverflow.net/a/154459/89334