Recent progress in Zauner's conjecture has leveraged deep conjectures in algebraic number theory to promote numerical line packings to exact and verifiable solutions to the line packing problem. We introduce a numerical-to-exact technique in the real setting that does not require such conjectures. Our approach is completely reproducible, matching Sloane's database of putatively optimal numerical line packings with Mathematica's built-in implementation of cylindrical algebraic decomposition. As a proof of concept, we promote a putatively optimal numerical packing of eight points in the real projective plane to an exact packing, whose optimality we establish in a forthcoming paper.