Folklore has it that it is impossible to define a well-ordering of the reals explicitly.
There exist pointwise definable models of ZFC where every set is definable without parameters: it is the unique element of the model that satisfies some finite formula $\varphi(x)$. So there is a formula $\varphi(x)$ such that $$ \tag{*} \forall x(\varphi(x)\rightarrow x\text{ well-orders }\mathbb R) \land \exists ! x\,\varphi(x) $$ is consistent with ZFC. (And it is not difficult to write down a concrete $\varphi$ which will work in a model with $\mathbf V=\mathbf L$).
Is it known that there is no $\varphi(x)$ such that $\text{(*)}$ is a theorem of ZFC?
Of course, since there are models of ZF that don't have a well-order of $\mathbb R$, in such a model $\varphi(x)$ would either be unsatisfiable or be satisfied by something that doesn't well-order $\mathbb R$. So the Axiom of Choice would have to be used in some essential way in the proof of $\text{(*)}$. But that doesn't in itself seem to preclude the possibility that $\varphi$ might exist.
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:
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)$.