I'm interested in equational logic which is the fragment of classical logic with only $\forall$ and $=$ as logical symbols and nothing else. In contrast with the logic described in the Wikipedia article, I disallow $\varphi \leftrightarrow \psi$ where $\varphi$ and $\psi$ are both propositions, despite the obvious analogy between $\leftrightarrow$ and $=$.
I'm mostly interested in this logic in the context of writing a simple proof assistant as a learning exercise. To that end, I'm trying to come up with some interesting dedicated tactics for natural fragments of first-order logic.
However, I learned in this comment by Z.A.K. on this question that there are some statements in ring theory with short proofs using ideals but no known equational proofs.
I'm wondering whether there's a good motivating example, ideally written out as an equation explicitly, of a statement in the language of rings with either A) no known equational proof or B) an equational proof that is much, much longer than the human proof.
I am interested in commutative algebra and ring theory as well, so understanding what kind of savings you get from using human-friendly tools is also interesting in its own right, not just instrumentally useful in understanding the limitations facing a potential proof assistant.
A later comment mentions $[a\iota(x), b\iota(y)] \vdash [\iota(x), \iota(y)]$ but my understanding of group theory is weak so I don't know how to translate that into the language of groups, and, if I'm reading it correctly, it's an entailment not a single equation in the language of an algebraic structure.
It is possible that some or all of the hard cases are entailments in the language of rings and not single equations. Those are also interesting, but I'm primarily interested in single equations.
Best Answer
Take the language of rings, and consider the algebraic structure (called an $n$-ring) whose axioms are the usual axioms for not-necessarily-commutative rings, along with the equation $x^n = x$ for some fixed large integer $n$.
Every $n$-ring satisfies the equation $xy=yx$.
This is known as Jacobson's theorem. For $n$ larger than 2, the known equational proofs are very long. For sufficiently large $n$, nobody ever succeeded in constructing an equational proof. You can read more about this phenomenon (and explore some constructions) in Martin Brandenburg's excellent article on the subject.
This is a motivating example, written out as an equation explicitly in the language of rings, so answers your question.
Aside: the distinction you draw between "single equations" and "entailments in the language of rings" is immaterial in the equational setting. A "proof of an entailment" $\Gamma \vdash x = y$, where $\Gamma$ is a set of universally quantified equations in the language of rings is the same as a proof of the equation $x = y$ in all $\Gamma$-structures in the language of rings. It makes no difference. For example, an equational proof that $0-(x + y) = (0 - x) + (0 - y)$ holds in all rings is exactly the same thing as a proof of the entailment $\Gamma \vdash 0-(x + y) = (0 - x) + (0 - y)$ where $\Gamma$ consists of the ring axioms.
The example I gave with commutators in the linked thread is similarly a proof of a single equation in a class of algebraic structures. However, it does not merely use the language of groups: it uses a richer extension of the language of groups, with two new constant symbols $a,b$ and two new function symbols $\iota$ and $\iota^{-1}$. You cannot translate it into the language of groups, because it's written in a different, richer language.
Note that if you intended to restrict the question to actual identities in the equational theory of rings with no additional axioms, then there can be no examples of such equations. Using the ring axioms you can algorithmically transform all equations into normal form $p(x,y,\dots) = 0$ for a polynomial $p$ in standard form, and an equation is universally true in the equational theory of rings precisely if $p$ is syntactically the zero polynomial (in which case $0=0$ concludes your equational proof).