Let Multipoint Arithmetic Circuit Evaluation (MACE) be the task of evaluating an multivariate arithmetic circuit of size $s$ (made of plus and times gates) on $s$ arbitrary inputs. We present a new (probabilistic) proof system for MACE which saves roughly a quadratic factor over the obvious $O(s^2)$ time algorithm when the circuit has low degree. There are many corollaries. Of particular interest to this crowd is that there is a proof system for counting SAT assignments to arbitrary Boolean formulas of $n$ variables and $2^{o(n)}$ size, where the proofs are of length about $2^{n/2}$ and the proofs can be verified (using $O(n)$ random bits) in about $2^{n/2}$ time with high confidence. In particular, UNSAT for arbitrary Boolean formulas can be verified by proofs of this length and with this running time. This result strongly refutes a "Merlin-Arthur Strong Exponential Time Hypothesis" which had been informally conjectured in the theory community. (Previously appeared in the 2016 Computational Complexity Conference.)