Let $A$ be an abelian variety over a field $K$. Let $B,C\subseteq A$ be abelian subvarieties.
1) When people write $B+C$, do they mean something like the smallest abelian subvariety containing both $B,C$? What is the formal definition of such thing?
2) Does $(B+C)(\overline{K})=B(\overline{K})+C(\overline{K})$ as groups?
2) Is it true that $\dim (B+C)\leq\dim B+\dim C$?
I have not studied this before, but my guess is that it is defined as the scheme theoretic image of the map $$B \times C \subseteq A \times A \stackrel{\mu}{\longrightarrow} A,$$ where $\mu$ is the group law. Since $A$ (and thus also $B$ and $C$) is projective (hence proper), the set-theoretic image is closed, and it carries the reduced induced structure since $B$ and $C$ do (Hartshorne, Exercise II.3.11 (d) and Exercise II.4.4). Then you should check that it is an abelian subvariety; the main point is to show it is closed under the group law. This should follow from the diagram-theoretic formulation of associativity. (Please verify; I did not check this in complete detail.)
Since the scheme-theoretic image is the set-theoretic image (which you can, in turn, relate to the image on $\bar K$-points), the answer to your second question is yes.
The third question also becomes easy: the dimension of a scheme-theoretic image is at most that of the source.