Recently, I have proved that Kazhdan's property (T) is theoretically provable
by computers ([arXiv:1312.5431](https://arxiv.org/abs/1312.5431),
explained below), but I'm quite lame with computers and have
no idea what they actually can do. So, my question is how feasible is it to
prove property (T) of a given group, say $\mathrm{Out}(F\_{r>3})$ (a famous
open problem), by solving the equation below by a computer? Even the case of
$\mathrm{SL}\_{r>2}({\mathbb Z})$ where property (T) is known is unclear.


A group $\Gamma$, generated by a finite subset $S$ and with its non-normalized Laplacian denoted by
$$\Delta=\sum\_{x\in S} (1-x)^\*(1-x)=\sum\_{x\in S} (2-x-x^{-1})\in{\mathbb Z}[\Gamma],$$
has property (T) iff the equation in ${\mathbb Z}[\Gamma]$,
$$ m \Delta^2 = n \Delta + \sum\_{i=1}^k l\_i \xi\_i^\*\xi\_i $$
has a solution in $k,m,n,l\_i\in{\mathbb Z}\_{>0}$ and $\xi\_i\in{\mathbb Z}[\Gamma]$.



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, <https://arxiv.org/abs/1411.2488>.


