In this paper, we are interested in the combination of abstract interpretation and interactive theorem proving, which stand at the opposite ends of the program verification automation spectrum. Our idea is to take advantage of the respective strengths of these two techniques. As a first case study, we focus on groundness analysis of logic programs. Using the proof assistant LPTP (Logic Program Theorem Prover), we automate the formal certification of groundness invariants generated by abstract interpretation. We present an experimental evaluation of our approach by applying it to a set of logic programs. Our experiments are twofold. On the one hand, to certify groundness invariants we use automated theorem provers drawing on the theoretical framework of LPTP. On the other hand, we generate and certify natural deduction proofs of groundness invariants with the proof checker of LPTP.