Do we know that we can't define a well-ordering of the reals?

The answer is that we can't write a formula which provably defines a well-ordering of $\Bbb R$ in $\sf ZFC$ (at least assuming that $\sf ZFC$ is consistent), although I don't know whose to credit for it.

Suppose that $\varphi(x,y)$ provably defines a bijection of $\Bbb R$ with an ordinal (this is equivalent to the way you state it, just making it easier to work with later on). Note that $\sf ZF$ proves that every well-ordering has a unique isomorphism with a unique ordinal, so it doesn't depend on anything.

Let $M$ be a countable transitive model [of enough axioms] of $\sf ZFC$. Consider the forcing which adds one Cohen real. The conditions of this forcing are finite functions $p\colon\omega\to2$ (here we mean partial functions, of course), ordered by reverse inclusion.

Denote by $\dot c=\{(p,\check k)\mid p(k)=1\}$ the canonical name for the Cohen real. Let $G$ be an $M$-generic filter, and let $c$ denote the interpretation of our Cohen real by $G$.

In $M[G]$ there is some $\alpha$ such that $M[G]\models\varphi(c,\alpha)$, therefore for some $p\in G$ we have that $p\Vdash\varphi(\dot c,\check\alpha)$.

Now pick any $m,n\notin\operatorname{dom}(p)$ and consider the permutation of $\omega$ which is the cycle $(m\ n)$. This permutation is in $M$, and we can apply it to the conditions of the forcing (by the action $\pi p(\pi n)=p(n)$). So we can think of it as an automorphism of the forcing. Some basic facts:

1. An automorphism of the forcing extends uniquely to an automorphism of the names.
2. $p\Vdash\phi(\dot x)$ if and only if $\pi p\Vdash\phi(\pi\dot x)$ for an automorphism $\pi$.
3. In the Cohen forcing, if $\pi$ is an automorphism induced as above by a permutation of $\omega$, and it is not the identity automorphism, then $1\Vdash\pi\dot c\neq\dot c$.
4. If $x\in M$, then $\pi\check x=\check x$, where $\check x$ is the canonical name for $x$.

We now have that $\pi p\Vdash\varphi(\pi\dot c,\pi\check\alpha)$. But $\pi p=p$, and therefore $p\Vdash\varphi(\pi\dot c,\check\alpha)$. Which is a contradiction since now $p\Vdash\varphi\text{ defines an injective function}\land\pi\dot c\neq\dot c\land\varphi(\dot c,\check\alpha)\land\varphi(\pi\dot c,\check\alpha)$.

Forcing with sufficiently homogeneous forcing that adds reals is enough to obtain the negation of $(*)$. The point is that if a formula $\phi$ defines a parameter-free well-ordering of $\mathbb R$, then for any ordinal $\alpha$, the statement "$x$ is the $\alpha$-th real in the well-ordering defined by $\phi$" uniquely characterizes $x$ in terms of $\alpha$. If the forcing we used is homogeneous, this implies that $x$ is in the ground model, as you can then proceed to uniquely characterize $x$ (for instance, you can verify whether "its first digit is $0$", "its second digit is $1$", etc). The way that homogeneity is used is in noticing that all these statements I am writing have the form $\psi(\check t_1,\dots,\check t_n)$ when written in the forcing language (for some $\psi$ in the language of set theory, and some $t_1,\dots,t_n$ in the ground model). But any such statement is either always or never forced (by homogeneity), and so, from the ground model, you can read off every real in the extension, so the forcing cannot add reals.

So you are done once you find a homogeneous forcing that adds reals. Cohen forcing is an example. One can go further and obtain models where there are no well-orderings definable using parameters from the ground model by a simple extension of the sketch above, and even models where there are no well-orderings definable, even if (ordinal definable, or small-sized) parameters from the extension are allowed (though now we need to add more than just one Cohen real to achieve this).

Since many natural forcing posets are sufficiently homogeneous to carry out the arguments just described, one of the surprising realizations that has come out of the study of forcing axioms is that they tend to imply the existence of definable well-orderings (either from a parameter, or even parameter-free if we force from a definable inner model). I have a few papers explaining this phenomenon, or see this talk. Some questions remain; for instance, it is still open whether if Martin's Axiom holds and $\omega_1=\omega_1^L$, then there is a projective well-ordering of the reals. In the early 2000s, I would have thought asking this was ridiculous. But we do not know.