Since this question made it back up to the top, let me take a stab. In short, there is going to be no air-tight definition of a "proof assistant" just like there is no air-tight definition of a "programming language". Sure C and Python are probably square in the programming language camp, but what about Brain F***, LaTeX, HTML, SQL, YAML, and some arbitrary macro language? What makes one a programming language and not the other?
The main thing I would say that makes a proof assistant (PA) a proof assistant is intent. That is a PA is indented as a way to assist the user in writing proofs. PAs are also called Interactive Theorem Provers (ITPs), with the same idea: An ITP is intended to be used as an interactive tool for proving theorems (as opposed to an Automated Theorem Prover).
The main area of interactive assistance that a PA/ITP provides is checking the details of a proof. For some proof assistants this checking is (mostly) air-tight logic. (For other, more experimental, proof assistants the user has to be more careful to avoid known inconstancies or unsoundness, but the intent is the same. If you use it as intended it will help you make sure you are following the rules of your proof system. This is even more important with experimental logics since one hasn't built up a good intuition yet of what is and isn't ok.)
Of course, in theory (and maybe even in practice already) it is possible to blend PAs with related tools like markup/document languages, specification languages, programming languages, automated theorem provers, computer algebra systems, and computer games. So it is really a continuum. But let's look at each of these technologies and see how they differ from PAs even if it possible to combine both intents into one tool.
Proof assistants are intended to build and record proofs. The the proofs (and even moreso the theorem statements) need to be written and stored in a human readable way so that (1) the user can enter the proof and (2) the user can find theorems to use for later proofs. (By "human readable", I mean at least as human readable as a computer programming language.) So in that way proof assistants are starting to resemble other tools for writing mathematics, like LaTeX and MathML. But the intent of proof assistants is different. LaTeX's and MathML's intent is focused more on presentation and document creation, whereas a proof assistant is focused on checking. In particular, Latex code has little semantic meaning. It is more focused about how the formula looks on a page.
Of course, there is a spectrum and the two can even be combined. While wome proof assistants like MetaMath provide very little pretty printing, other's like Lean have good unicode support (often borrowing LaTeX keywords) to make the code look more like mathematics. Further, I believe there are tools already (maybe for Mizar and Isabelle/Isar if I remember correctly) to export a PA proof into something more like natural language LaTeX or HTML. Also, Coq has a tool (whose name I forget) for turning Coq files into something more like HTML notebooks (not unlike Jupyter notebooks combine Python code and Markdown into a single readable code document). Moreover, there is no reason to think in the distant future that if proof assistants improve enough, everyone would write their proofs in a language which simultaneously makes a readable and publishable document along with a completely checked proof.
Specification and data transmission languages
One aspect of a proof assistant is just providing a way to write mathematics in an unambiguous way. With such a language one can completely and unambiguously write specifications (say for a computer chip), record mathematical knowledge, and record complex interactions between objects in a dataset (similar to, but beyond, how current knowledge graphs already store some first-order logic relationships between nodes in the graph). Very simple specification languages like JSON, YAML, and Protobufs are mostly for data, but with a PA's language you can add in conditions, relationships, functions, etc.
I would say this is more of a side effect of PAs than their intent, but we will see if this becomes important. Then more work might take off in this area. Also, Tom Hales and associates are working on a controlled natural language for mathematical statements. If say this controlled natural language only lets you write math statements, but not proofs (or doesn't check the proofs), is it a proof assistant? Likely not. It would say it would be something new.
Some may be confused by the current crop of dependent type theory (DTT) proof assistants like Coq, Agda, Lean, etc. These are interesting because DTT is intended as both a way to check proofs and as a way to write computer programs. From the abstract to Martin-Löf's 1982 paper Constructive mathematics and computer programming:
If programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation [...], then it no longer seems possible to distinguish the discipline of programming from constructive mathematics. This explains why the intuitionistic theory of types [...], which was originally developed as a symbolism for the precise codification of constructive mathematics, may equally well be viewed as a programming language.
Coq, Lean, and Agda have all capitalized on this propositions-as-types correspondence but in slightly different ways. (I don't know enough Agda to say anything about it here except that Wikipedia calls Agda a programming language.) The pure programming language given by intentional type theory has a major difference between other programming languages. Every function must be proved to be total, so it is impossible to write an unbounded search (such as counting the number of steps of the Collatz conjecture recurrence until one gets to 1 without proving the Collatz conjecture). Hence pure DTT is not Turing complete.
Both Coq and Lean (and likely Agda) use the ability to prove judgmental equalities like
1 + 0 = 1 by just computing (or reducing) both sides. For Coq especially this is really powerful. If I understand correctly, the 4 color theorem proof in Coq was mostly a giant definitional equality proof.
Lean 3 and Lean 4 also provide a way to make impure functions which share the same language as the pure Lean functions (including the ability to call pure functions inside impure functions). This lets one also use Lean to write regular computer code with unbounded searches, infinite loops, and possibly non-terminating recursion. As for intent, Lean 3 seems to intend that these
meta functions as a meta language for, say, writing tactics. (Coq on the other hand has a separate tactic-writing meta-language different from pure Coq.) Lean 4 however intends to be a full programming language as well as a full proof assistant. As such Lean 4 also has good support for IO, hash tables, reading and writing with arrays, floating point computation, and the like. But to be clear, Lean doesn't run most of this code in the kernel, but in a VM (for Lean 3) or as compiled code (for Lean 4). In that way, it is more that Lean the programming language and Lean the proof checker are using the same syntax, but using different back ends to do the computation.
While most functional languages are not dependently typed, it is still possible to use say Scala, OCaml, or Haskell as proof checkers for propositional logic. For example, in Scala the fact that I can write a function for
def foo[A, B]() : A -> B -> (A, B) with no special tricks shows that
A -> B -> (A and B) is constructively provable. The issue of course is that this is not the intent of Scala. Moreover, Scala provides lots of unsafe tools like type casting, non-polymorphic handling of specific types, and unbounded recursion which would make it possible to give a program for
def law_exluded_middle[A]: Or[A, A -> Empty] which compiles (although that program would likely crash if I ran it).
Other proof assistants like Isabelle also have the ability to generate code. This isn't exactly the same as a programming language, but again the boundaries are blurred.
Automated theorem provers
My understanding is that automated theorem provers (ATPs) actually came before ITPs. As the name suggests ATPs are intended for automated creation of proofs, where as ITPs are intended for interactive creation of proofs. The lines definitely get blurry here. On one hand Metamath has almost no automation. The proofs are just entered by hand. On the other hand, Isabelle's Hammer provides automation on the level of an ATP (mostly because it uses an ATP in the background). In the middle, tactic-based theorem provers like HOL-Light, HOL4, Isabelle, Lean, and Coq all allow whatever automation is in the tactics, and in many it easy to write custom tactics.
To say that ATPs have no interaction is also likely not totally true. If nothing else, some ATP users have a great skill of manipulating a problem into a form where it can be solved with an ATP. That is a form of interaction.
Also, as machining learning based AI is starting to get into the theorem proving game, they often interface with ITPs instead of ATPs. In some ways, one can view the AI agent as taking the role of the human in the human-computer interaction. Since ITPs are already interactive, they are a great starting point for the back and forth interaction that an AI agent requires. Moreover, ITPs have a large amount of human-created proof data to train from. Last, the automation needs in ITPs (like creating induction proofs, library search, or doing obvious steps) are often different from the types of proofs that a typical ATP can handle well. I wouldn't be surprised to see a "proof assistant" in the future which isn't designed at all for human assistance, but just for assisting an AI agent. (Actually I would already put toy AI theorem proving environments like INT and (the backend of) rlCOP in this category.)
Computer Algebra Systems
What distinguishes a proof assistant like Lean from computer algebra system (CAS) like Mathematica is again the intended use case. Mathematica is intended for calculating with symbolic mathematical objects. While any programming language could have a library which does this sort of thing (and Python does have a few such libraries) a CAS is specialized for this purpose with often decades of prior work put into it.
However, the trade off is that CASs are not typically built with the assurances of theorem provers. There are known bugs in these systems and often they don't generate anything resembling a proof. There have been a number of papers discussion the idea of combining the two systems, either by (1) building a CAS on top of a proof assistant or (2) interfacing the two so that a CAS proves a witness/answer/proof which can be checked by the proof assistant.
It should also be mentioned that even though, say, Lean has (1) lots of mathematical objects, and (2) a full computer language, it doesn't mean Lean has good support for the kind of computations done in CASs. The issue is many-fold, but one basic problem is that the best definition (of say a polynomial) for proving may not be the best definition for computation. This is just an engineering challenge, which could in theory be solved with enough work, but it is a challenge none-the-less.
I don't think anyone would confuse a proof assistant for a computer game, but at the same time why not? Many computer games are puzzles. The user interacts with a puzzle environment (like in "Baba is You") and has to follow the rules to get to the desired goal. Many people have commented on the similarities, and some learning resources like the Natural Number Game are specifically build around a game mechanic to make the learning more fun. Again, it is all a matter of perspective and intent.
Ad hoc proof finding code
The first 4 color theorem proof, as well as each proof finding the highest known prime number, uses computers to find a proof. The big difference between PAs is that proof assistants are general purpose. This generality makes the proofs more likely to be correct. A good analogy is that the proof-checking kernel in a PA is more like a programming language compiler, whereas the original four color theorem computer proof is more like a bespoke program. It is rare to encounter bugs in a compiler but quite common to find bugs in a program. By moving all the important parts of the computation to a small trusted computing base, it makes proof assistants more reliable than ad hoc code which checks millions of cases.