Is the following true (and if yes, where the best proof is written?)? For any $c>0$ for large enough positive integers $N$ we have $\sum_{k=0}^{N-1} \cos(k^2t)\geqslant -cN$ for all real $t$? Hm, if true, it should be hard: it allows to get signs of certain Gauss type sums, for example.