Many problems, including the correctness of software, or the truth of mathematical theorems (e.g. Kepler's conjecture) reduce to proving that a real function satisfies some bound on a domain. A numerical global optimization tool, however, might not provide the assurance needed: it may itself contain bugs, or suffer from floating-point round-off errors. We would like the tool to provide a proof witness, independently verifiable by a simple checker (such as the type checker at the core of the Coq proof assistant). We thus seek to obtain witnesses checkable by a Coq script for the following problem: assuming $P_1\ge 0 \ldots P_n\ge 0$ prove $Q\ge 0$ (and variants with equalities and/or strict inequalities). This problem reduces to finding sums of squares (SOS) of polynomials that satisfy some linear equality (Positivstellensatz). Finding SOS reduces to feasibility in semidefinite programming, for which there exist numerical solvers. Unfortunately, the solution set can have empty interior, in which case numerical solvers (based on interior points) fail. Previously published methods thus assumed strict feasibility; we propose a workaround for this difficulty. The trick is to use approximate numerical solutions to find a parametrization of the linear affine variety generated by the solution set: we obtain one (assuming one exists with small integer coefficients) by repeat search of short vectors in lattices, using the algorithm of Lenstra, Lenstra \& Lovasz (LLL).