The field of theorem proving develops techniques for conducting mechanical proofs with all the rigor that a formal proof in a proof calculus enables. The field of computer algebra develops techniques for symbolic computations that generalize beyond particular numerical quantities. Computer algebra and theorem proving meet in many ways, including in the Calculemus eforts and in the foundational realization that computation and deduction obey fundamental dualities. Both fields integrate particularly prominently in theorem proving for hybrid systems, which are dynamical systems mixing discrete and continuous dynamics, because verified insights that generalize to the uncountable domain beyond finitely many particular numerical test cases are particularly valuable. With formally verified quantifier elimination in real-closed fields, for instance, both fields forge an undeniably close inherent bond. This talk will share some insights from these fields, while identifying interesting scientific opportunities along the way.