How feasible is it to prove Kazhdan's property (T) by a computer?

Using the $\Delta^2- \epsilon \Delta$ approach, Tim Netzer and I have verified Kazhdan's property (T) for ${\rm SL}(3,\mathbb Z)$. For the standard generators $e_{ij}$ ($i\neq j$) we can show a spectral gap of the normalized Laplace operator of $1/120$. There is a lot of room for further improvement.

To my knowledge, the best previously known lower bound was about $1/3500000$ (and the best upper bound $1/3$).

The approach uses a positive semi-definite programming package in MatLab, which we use to guess a large positive semi-definite matrix and Mathematica to verify symbolically (computing with fractions etc.) that this indeed yields a sum-of-squares decomposition + some easy theoretical argument that deals with the error terms. The final argument is purely symbolic and does not involve any numeric computation that could involve errors because of rounding etc.

We are planning to write a short note and make the computation available in the internet. Now, we attempt to see what we get for ${\rm Aut}(F_4)$.

Edit on November 11, 2014: We have now uploaded the preprint with an attached Mathematica notebook to the arXiv, http://arxiv.org/abs/1411.2488.

I can make a little progress here. One of your key subproblems is: Given a computable group $G$, a finite list of elements $T \subseteq G$ and an element $\alpha \in \mathbb{Q}[G]$, determine whether there exist $\xi_1$, $\xi_2$, …, $\xi_k$ in $\mathbb{R} T$ so that $$\alpha = \sum_{i=1}^k \xi_i \xi^{\ast}_i.$$

This problem can be solved by semidefinite programming, which is a field of numerical analysis with well developed toolkits. In particular, I will solve the above problem for all $k$ at once.

Write the elements of $T$ as $g_1$, $g_2$, ..., $g_t$ and write $$\xi_i = (g_1 \ g_2 \ g_3 \ \cdots \ g_t)^T \cdot a_i$$ where $a_i \in \mathbb{R}^t$. Then the above equation is $$\alpha = (g_1 \ g_2 \ g_3 \ \cdots \ g_t)^T \left( \sum_{i=1}^k a_i a_i^T \right) (g_1^{-1} \ g_2^{-1} \ \cdots \ g_t^{-1} ).$$

Recall that a $t \times t$ real matrix $X$ can be written as $\sum a_i a_i^T$ if and only if $X$ is positive semidefinite. So your question is does there exist a matrix $X$ such that

(1) $X$ is positive semidefinite and

(2) $\alpha = (g_1 \ g_2 \ g_3 \ \cdots \ g_t)^T X(g_1^{-1} \ g_2^{-1} \ \cdots \ g_t^{-1} )$

Note that condition (2) is an affine linear condition on $X$. Solving linear equations with the constraint that variables be positive semidefinite matrices is what SD programming is all about.

Working a little bit harder, you should be able to copy Peter Shor's trick here and maximize $r$ subject to the SD program $$\Delta^2 = r \Delta + (g_1 \ g_2 \ g_3 \ \cdots \ g_t)^T X(g_1^{-1} \ g_2^{-1} \ \cdots \ g_t^{-1} ),\ X \ \textrm{positive semi definite};$$ so you get a spectral gap if the optimal $r$ is positive.

I expect the hard part will be choosing the set $T$ to use; I have no ideas about this.

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, as suggested by David Speyer in his answer.

It is now known that the group $\mathrm{Aut}(F_n)$ has property (T) iff $n\geq 4$.

For $n\geq 5$ this is shown in Kaluba-Kielak-Nowak. The case $n=5$ was treated earlier in Kaluba-Nowak-Ozawa and the case $n=4$ was recently settled in Nitsche. Some earlier positive results were obtained in Netzer-Thom and Fujiwara-Kabaya. $\mathrm{Aut}(F_2)$ and $\mathrm{Aut}(F_3)$ are known not to have (T). This is all quite remarkable.