The first few values of Rayo's function? Rayo's function defined in English:
"$\operatorname{Rayo}(n)$ is the smallest positive integer bigger than any finite positive integer named by an expression in the language of first order set theory with $n$ symbols or less."
More formally, we make use of the following second-order formula (Sat):
∀R {
{for any (coded) formula [ψ] and any variable assignment t
(R( [ψ],t) ↔
( ([ψ] = `x_i ∈ x_j' ∧ t(x_1) ∈ t(x_j)) ∨
([ψ] = `x_i = x_j' ∧ t(x_1) = t(x_j)) ∨
([ψ] = `(∼θ)' ∧ ∼R([θ],t)) ∨
([ψ] = `(θ∧ξ)' ∧ R([θ],t) ∧ R([ξ],t)) ∨
([ψ] = `∃x_i (θ)' and, for some an xi-variant t' of t, R([θ],t'))
)} →
R([φ],s)}

where [φ] is a Gödel-coded formula and s is a variable assignment.
We then define $\operatorname{Rayo}(n)$ as:
The smallest number bigger than every finite number m with the following property: there is a formula φ(x) in the language of first-order set-theory (as presented in the definition of `Sat') with less than or equal to $n$ symbols and x as its only free variable such that: (a) there is a variable assignment s assigning m to x such that Sat([φ(x)],s), and (b) for any variable assignment t, if Sat([φ(x)],t), then t assigns m to x. 
I do wonder, how many values of this function are explicitly known or have good bounds?  For example, for $0\le n<10$, I speculate that $\operatorname{Rayo}(n)=0$, since it takes, I believe, ten symbols to write zero.  Once we write zero, we get $\operatorname{Rayo}(10)=1$, and so on.  So how many values can we reach?

I have not seen any good references for this.

Related: Is Rayo's number really that big?
 A: Your question is about what I view as the definable-in-set-theory
analogue of the busy beaver problem. I had previously posted an
answer on MathOverflow to the corresponding question concerning
what I view as the definable-in-arithmetic analogue of the
busy-beaver function. The
main conclusion there was that this function has a growth rate
exceeding any arithmetically definable function, and furthermore,
that the function is not itself arithmetically definable.
A similar analysis works for your function.
The first thing to notice is that what you call the Rayo function
is not definable in the first-order language of set theory.
Basically, you haven't actually defined a function, because the
concept of which numbers are definable or not is not expressible in
the same language.
But in second-order set theory, or at least in the set theory
having a proper class truth predicate, then we can define the Rayo
function, by reference to that truth predicate. Such a predicate,
for example, is provable in Kelley-Morse set theory, as I explain
in my blog post Kelley-Morse implies con(ZFC) and much
more.
So let us work in the theory GBC + Tr is a satisfaction class or
truth predicate for first-order set-theoretic truth. With this
class, the Rayo function $R(n)$ is definable, since we can refer to
the truth predicate to find out which functions are definable.
Theorem. The function $R(n)$ eventually dominates every
set-theoretically definable function.
Proof. Suppose that $f:\mathbb{N}\to\mathbb{N}$ is a set-theoretically
definable function, so that the relation $f(x)=y$ is definable in
the language of set theory by some formula $\varphi(x,y)$.
Notice that with the powers of two, we can easily define large
numbers with comparatively small formulas. For example, $2^n$ is
definable by a formula of size $n+c$ for some constant $c$. Put
differently, and by iterating this, for any sufficiently large $k$
we can define a number $k^+$ larger than $k$ with a formula smaller
than $\log(\log(k))$.
Therefore, if $k$ is very large with respect to these constants and
the size of the definition of $f$, then we can define $\max_{x\leq
k^+}f(x)$ using a formula of size less than $k$. Thus, $f(k)\leq
R(k)$, as desired. QED
Corollary. It is not possible to provide a first-order set-theoretic 
definition of the Rayo function.
Proof. If you could define it, then add one, and this would be
a definable function not dominated by the Rayo function, contrary
to the previous theorem. QED
In particular, we cannot define this function in ZFC set theory,
and I don't find it meaningful to talk about the Rayo function in a
general mathematical context without further specifying the
foundational context, such as whether there is a truth predicate
available or not.
For example, the formal definition that you provided from the link involves a second-order quantifier $\forall R$, but it will not work in all models of second-order set theory GBC, since it presumes that there is a truth function. But it will work in Kelley-Morse set theory or in GBC + Truth predicate. One can improve the definition somewhat by asking for $R$ to be only a partial satisfaction class, defined on all formulas of complexity less than $n$, and then you'll get a definition that works in GBC, but it will not be provably total, although it will be defined on the standard finite numbers. But GBC is not strong enough with separation for the function to exist as a set, since it is being defined with a second-order quantifier. 
Meanwhile, however, your actual question is about small values of
$n$, and in this case, if one is referring only to a bounded part
of the Rayo function, then the question is perfectly sensible,
since for every particular finite $n$, we have a $\Sigma_n$ truth
predicate and a way of referring to truth defined by formulas of
size at most $n$. And so one can still hope to prove lower bounds
for $R(n)$ for various small values of $n$.
In particular, for the Rayo number itself, which takes $n$ as a googol symbols, the function is definable. 
But let me point out further that once $n$ gets to have sufficient size, then the values of $R(n)$ will become independent of ZFC. For example, in set theory,
we can define a number $k$ to be the smallest such that $2^\omega$
has size $\aleph_k$, if there is such a finite number $k$, and
otherwise $0$. The point now is that this defines a definite number in set theory, but ZFC does not settle what the value is or provide any upper bound in
the natural numbers. For this reason, after a few steps, the nature
of the function $R(n)$ becomes completely wrapped up in the
meta-mathematical foundational issues I have alluded to earlier.
In particular, since I believe that the definition I provided can be made formally in fewer than a googol symbols, the particular value of Rayo's number, R(googol), is independent of ZFC, and no upper bound can be proved in ZFC for it.
