What are formal symbols at the definition of a divisor of an elliptic curve

An elliptic curve $E$ is locally given by polynomial equations, something like $y^2=x^3+ax+b$. If the coefficients $a$ and $b$ are in some field $K$, then we say $E$ is defined over $K$. If $\overline{K}$ is the algebraic closure of $K$ then "$\overline{K}$-points", denoted $E(\overline{K})$ in the power point, are pairs $(x,y)$ solving by the equation $y^2=x^3+ax+b$.

Divisors are simply the free abelian group of the points. So take the free abelian group whose basis is indexed by points on. The "formal symbol" is just referring to the basis element defined by each point.

The coefficients aren't determined, a divisor just is some finite list of points with an integer attached to each. There are various reasons to be interested in divisors however. Lets look at something that isn't quite an elliptic curve but is still an algebraic curve, the affine line $\mathbb{A}^1_{\overline{K}}$. Let $f$ be a rational function on $\mathbb{A}^1_{\overline{K}}$, so some function like: $$ f(x)=\dfrac{(x-1)(x-4)^2}{(x-2)^3(x-7)} $$ we say $f$ has a zero of order 1 at 1, a zero of order 2 at 4, a pole of order 3 at 2, and a pole of order 1 at 7. We can then define the following divisor $[1]+2[4]-3[2]-[7]$. This divisor keeps track of where $f$ is zero and undefined, and this construction can be generalized to any algebraic curve, this allows us to use divisors to study rational functions on a curve. Such divisors are called principle divisors and if you quotient out by the subgroup of priniciple divisors you get something called the Picard group of which will classify line bundles on your curve. In the power point it says that degree 0 divisors modulo principle ones are isomorphic to the group of $\overline{K}$-points. I don't think of anything other than a $\mathbb{Z}$-linear combination of points, but divisors are interesting for many reasons.