Why does the definition of addition require proofs?

We don't have to simply define addition and hope we get it right. We can actually prove the existence a uniquely defined add function on $N$ with all the required properties.

We can formally construct the $add$ function on the set of natural numbers $N$ by selecting the following subset of $N^3$:

$\forall a,b,c:[(a,b,c)\in add \iff (a,b,c)\in N^3 $

$\land \forall d\subset N^3:[\forall e\in N:(e,0,e)\in d\land \forall e,f,g:[(e,f,g)\in d \implies (e,S(f),S(g))\in d]$

$\implies (a,b,c)\in d]]$

where $S$ is the successor function on $N$ given by Peano's Axioms.

Using Peano's Axioms, we can prove that the set of ordered triples $add$, so defined, is a function such that, using the prefix functional notation, we have:

$\forall a,b\in N: add(a,b)\in N$

$\forall a\in N:add(a,0)=a$

$\forall a,b\in N:add(a,S(b))=S(add(a,b))$

We can also prove that the $add$ function, so defined, is unique. If $add'$ is another function such that we also have:

$\forall a,b\in N: add'(a,b)\in N$

$\forall a\in N:add'(a,0)=a$

$\forall a,b\in N:add'(a,S(b))=S(add'(a,b))$

then we can prove by induction that $\forall a,b\in N: add(a,b)=add'(a,b)$

We then feel justified referring to the add function + (using the infix notation) where

$\forall a,b\in N: a+b\in N$

$\forall a\in N:a+0=a$

$\forall a,b\in N:a+S(b)=S(a+b)$

The proof is necessary to ensure that the definition is actually meaningful.

Suppose, for instance, that I define a binary operation $\circledast$ on $\mathbb{Q} \times \mathbb{Q}$ as follows: For any rational numbers $q_1$ and $q_2$, I say that $q_1 \circledast q_2$ is the smallest rational number greater than $q_1 \cdot q_2$. Great! Only problem is, no such smallest rational number exists.

Second example: I define a ternary operation $F$ on $\mathbb{R} \times \mathbb{R} \times \mathbb{R}$ as follows: $F(a,b,c)$ is the solution to the equation $a x^2 + bx + c = 0$. Terrific! Only problem here is, sometimes no such solution exists, and sometimes more than one solution exists.

Whenever you define something, it's essential to prove that the thing being defined both exists and is unique. Otherwise the definition is meaningless.