Unfortunately there is much less code reuse possible than one would hope.
There three levels to consider:
- Differences between mathematical foundations (and implementations) between proof assistants.
- Differences between mathematical foundations (and implementations) between automated theorem provers.
- Differences between the approaches taken to develop a proof assistant and an automated theorem prover.
One would hope that at least for 1. and 2. the code should be reusable, but it very much depends on the mathematical foundation chosen for the PA (or ATP). For instance, Coq is based on the type theory called Calculus of Inductive constructions, while Agda is based on Martin-Löf type theory - this means that proofs may not be fundamentally compatible (i.e. a theorem may hold in one type theory, but not in the other), let alone the fact that Coq and Agda use very different syntax (making actual code reuse infeasible). There are steps being taken towards translating proofs from different foundations (for instance , ), but there is a lot to be said there.
A similar problem occurs in ATPs, although there at least the input format (specification of a conjecture to be proven) is somewhat standardised, mostly they use the TPTP format  (and the TSTP format for proofs).
For 3. (differences between ATPs and PAs), there is the problem, that ATPs and PAs are addressing a different problem: while proof assistants aim to check proofs, automated theorem provers aim to automate producing proofs. For this reason, most PAs are based on type-theory (dependent types enable better expressivity for the problems at hand), while ATPs are mostly dealing with first-order logic, or "simple theories" (linear arithmetic, theory of arrays etc.) supported by SMT solvers - theories where we can reason by refutation and the currently available automation techniques (tableaux method, superposition calculus, ...) can be used.
However, there are projects aiming towards importing proofs produced by ATPs (usually the TSTP trace) into some proof assistants for re-checking, for instance Ekstrakto [4,5] and TESC [6,7].
 The Dedukti logical framework: https://deducteam.github.io
 Anja Petković Komel: Meta-analysis of type theories with an application to the design of formal proofs, PhD thesis, University of Ljubljana, 2021. URL: https://anjapetkovic.com/img/doctoralThesis.pdf
 Thousands of Problems for Theorem Provers: https://www.tptp.org/
 Yacine El Haddad. Integrating Automated Theorem Provers in Proof Assistants. PhD thesis, Université Paris-Saclay, 2021.
 Ekstrakto URL: https://github.com/Deducteam/ekstrakto
 Seulkee Baek. A Formally Verified Checker for First-Order Proofs. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceed- ings in Informatics (LIPIcs), pages 6:1–6:13, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
 TESC URL: https://github.com/skbaek/tesc