  In this note we show that unsatisfiable systems of linear equations with a
constant number of variables per equation over prime finite fields have
polynomial-size constant-degree semi-algebraic proofs of unsatisfiability.
These are proofs that manipulate polynomial inequalities over the reals with
variables ranging in $\{0,1\}$. This upper bound is to be put in contrast with
the known fact that, for certain explicit systems of linear equations over the
two-element field, such refutations require linear degree and exponential size
if they are restricted to so-called static semi-algebraic proofs, and even
tree-like semi-algebraic and sums-of-squares proofs. Our upper bound is a more
or less direct translation of an argument due to Grigoriev, Hirsch and
Pasechnik (Moscow Mathematical Journal, 2002) who did it for a family of linear
systems of interest in propositional proof complexity. We point out that their
method is more general and can be thought of as simulating Gaussian
elimination.
