How Mathematica differs from proof assistants? Specifically - proof assistants can be used for embedding/implementing logics into them, like "Working with Linear Logic in Coq" http://www.cs.nuim.ie/~jpower/Research/LinearLogic/ and "Mechanizing Linear Logic in Isabelle" http://www.cl.cam.ac.uk/~lp15/papers/Workshop/papers/kalvala-linear.pdf. So - proof assistants can be used for creating theorem provers for specific logics. Can Mathematica be used for similar endeavours as well and maybe Mathematica is even better for such efforts? As far as I have searched, then there is no efforts to embbed some non-classical, exotic logics in Mathematics, so - choosing the proof assistants is the optimal way forward.
I guess one general difference is that Mathematica (may be) is not formally certified, it is just collection of ad hoc algorithms under common syntactic interface.
You can use any general purpose programming language you like as an implementation language for a proof assistant. Ed Clarke implemented a proof assistant called Analytica in Mathematica. There are no "formally certified" programming languages for implementing proof assistants, as far as I know. However, Mathematica is a large and complex programming language with a closed source implementation, so a proof assistant implemented in Mathematica would likely be considered less trustworthy than systems like Coq or HOL that are implemented in the LCF paradigm.