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.
The 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 is 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)$.