Negation of injectivity

By definition, $f$ is injective if and only if

$$ \forall(a,b) \in \mathbb{R}^2: f(a)=f(b) \implies a=b. $$

The negation of this statement is

$$ \exists (a,b) \in \mathbb{R}^2: f(a)=f(b) \quad \text{and} \quad a \neq b. $$

$f(x)=x^2$ is not injective because there exists the pair $(-1,1)$ such that $(-1)^2 = 1^2$ but $-1 \neq 1.$

There exists $a,b \in \mathbb{R}$ such that $f(a) = f(b)$ but $a\neq b$, is a negation of injectivity.

"P but not Q" so the formal definition of non-injectivity should be $f(a)=f(b) \implies a\neq b$, right?

Wrong, but close. You said "P but not Q" (which really means "P and not Q") and then you wrote the equivalent of "P implies not Q". These are different.

You also have to be careful how to take negation inside a quantifier. The definition of injectivity really is "for all $x,y$ something", which is negated as "there exists $x,y$ for which NOT something". Substituting "P implies Q" for "something", and using the rule for negating an implication, we get that the negation of "for $x,y$ P implies Q" is "there exists $x,y$ such that P and not Q".