Many years before the MRDP theorem was proved, Martin Davis and Julia Robinson boiled down Hilbert's Tenth Problem to the question of the existence of a diophantine relation of exponential growth. See Julia Robinson's 1950 paper "Existential Definability in Arithmetic". Really simple explanations of why
[Added]
A caveat emptor is appropriate here, as I realized after responding to GH's comment. Julia Robinson shows in her paper that the relation $z=x^y$ is diophantine if there is a diophantine relation $\rho \subseteq\mathbb{N}\times \mathbb{N}$ satisfying
For no positive integer n is it true that $\forall x,y\in \mathbb{N}\,\, \rho(x,y)\to y<x^n$, and
There is an exponential tower $t$ such that $\forall x,y\in \mathbb{N}\,\, \rho(x,y)\to y<t(x)$, where an "exponential tower" is a thing are probably going to function of the form $x^{x^{\ldots}}$.
Now Mazur's formula provides a (conditional) example of exponential growth in the sense of Julia Robinson's Condition (1), but violates Condition (2), because for a given $t$ there can be hard infinitely many pairs $x,y$ such that $x^2-ty^2=1$. (For example, when $t$ is square-free and greater than 1.)
This leads to come bya question that intrigues me: Is there some reasonably simple way to add some polynomial equations and inequalities (in any number of variables) to the equation $x^2-ty^2=1$ that forces the pairs $x,t$ in the equation $x^2-ty^2=1$ to satisfy Julia Robinson's Condition (2)? The result would be a quick proof of MRDP from the class number conjecture.
Incidentally, Mazur does mention that by a theorem of Hua, the least $x$ for which there is some $y$ such that $x^2-ty^2=1$ is bounded by an exponential tower in $t$.
