How can Busy beaver($10 \uparrow \uparrow 10$) have no provable upper bound?

This wikipedia article claims that the number of steps for a $10 \uparrow \uparrow 10$ state (halting) Turing Machine to halt has no provable upper bound:

"... in the context of ordinary mathematics, neither the value nor any upper-bound of $\Sigma(10\uparrow\uparrow10)$ can be proven..."

How is this possible? In principle, wouldn't listing the computations of all the (finitely many) halting Turing machines of that size, and individual proofs of non-halting for all the non-halting ones (again, finitely many) create a proof?

I'm assuming that the "ordinary mathematics" mentioned has no formal meaning.

The Wikipedia article explains exactly what it means. Here is an elaboration.

Define the complexity of a number $n$ to be the smallest number of states for a Turing machine that returns $n$ when run with $0$ as an input. Certainly every number has a complexity. Now let $T$ be any effective formal theory whose language includes statements of the form "$n$ has complexity greater than $k$" for each $n$ and $k$. Some of these sentences may be provable in the theory, and some may not. Say that the theory is complexity sound if each statement "$n$ has complexity greater than $k$" that is provable in the theory is correct. Both PA and ZFC are effective, complexity sound theories.

Theorem. For any effective, complexity sound theory $T$, there is some $k$ such that the theory does not prove that any number $n$ has complexity greater than to $k$.

Proof by contradiction. Assume $T$ is complexity sound and proves statements of the form "$n$ has complexity greater than $k$" for arbitrarily large $k$. Consider a program $P$ that does the following when run with $0$ as an input. First, $P$ computes its own source code (like a Quine; formally, the proof uses Kleene's recursion theorem). Then $P$ counts the number of states $s$ in this source code. Next $P$ enumerates all statements of the form "$n$ has complexity greater than $k$" that are provable from $T$, until it finds one with $k > s$. It will find one by assumption. Finally, $P$ returns $n$. Because $T$ is an effective theory, $P$ can do all this computably. But then the number $n$ returned is by $P$, which has $s$ states, but $T$ proves "$n$ has complexity greater than $k$" for some $k > s$, so $T$ is not complexity sound, which is a contradiction. That completes the proof.

Thus there is a bound on the largest $k$ such that $T$ proves "$n$ has complexity greater than $k$" for any $n$. In fact, we can actually write down $P$ explicitly, and thus $k$ is no more than the number of states of the version of $P$ we write down. For any reasonable theory, like PA or ZFC, this $k$ will be huge but not anywhere near $10\uparrow\uparrow 10$.

If a sufficiently strong theory cannot prove any $n$ has complexity larger than $k$, then it also cannot prove any statement of the form "$m$ is an upper bound on $\Sigma(k)$", because if it could prove that it would also prove "$m+1$ has complexity greater than $k$". So in particular neither PA nor ZFC can prove an upper bound on $\Sigma(k)$ when $k$ is sufficiently large.

Just as the Wikipedia article says, the theorem above is just a recasting of Chaitin's incompleteness theorem in which the length of the program is replaced with the number of states.

In fact, even $\Sigma(7918)$ has no provable upper bound in ZFC, assuming SRP is consistent.

This was shown by Adam Yedidia and Scott Aaronson. Aaronson talks about the result here.

They constructed a machine $Z$ that can't be proven to run forever in ZFC, but it does run forever assuming other axioms (Namely using the SRP (Stationary Ramsey Property)).

If $\Sigma(7918)$ had a provable upper bound in ZFC, then $Z$ could just be run for that amount of steps to prove it halts or doesn't halt. Contradiction.

While what has been discussed in the comments is relevant (there exist individual Turing machines which have undecidable Halting problems), I doubt this is what the statement in the Wikipedia article is referring to, mainly because there's absolutely no need to mention a bound as high as $10 \uparrow \uparrow 10$ to find a Busy Beaver with an undecidable Halting problem.

Any universal Turing machine has an undecidable Halting problem, for if it didn't, you would be able to solve the Halting problem for any machine it simulates. There are universal Turing machines with only a handful of states (see e.g. this paper of Neary and Woods.) The restriction that a Busy Beaver starts with a blank tape isn't of consequence, because the machine can just write a machine description onto the tape, and then proceed to simulate it.

I suspect the phrase "ordinary mathematics" is an oblique reference to first-order Peano Arithmetic or similar, and the statement is referring to some proof that any proof of a bound for TM's with $10 \uparrow \uparrow 10$ states must use transfinite methods, even if the TM is total (like the Hydra rewriting game, or something in a similar vein.) But this is just a guess.

("Ordinary mathematics" normally suggests ZFC to me, but a proof that this result is independent of ZFC would be somewhat too astonishing to me, for me to take that interpretation here.)

Here's a simpler argument that doesn't depend on explicit diagonalization. On the other hand, in contrast to Carl Mummert's answer it only works for first-order theories or another axiomatic framework where something like Gödel's completeness theorem holds. But that's enough to cover the usual suspects for "ordinary mathematics", i.e. PA and ZFC.

First, of course, fix a particular first-order theory $T$ that you want to prove the claim about. We assume it is effectively axiomatized and doesn't prove arithmetic falsehoods (in particular it is consistent).

Let $M$ be a Turing machine that loops through the natural numbers until it finds one that is the Gödel number of a proof of $T\vdash 0\ne0$, and then stops. Since "is the Gödel number of a proof of $T\vdash0\ne0$" is (primitive) recursive, there's certainly a Turing machine that does this, and it will have much fewer than $10\mathop{\uparrow\uparrow}10$ states. (The huge bound of $10\mathop{\uparrow\uparrow}10$ must be in order to cater for really wasteful ways to implement p.r. functions as Turing machines).

Now $M$ cannot ever halt, since we're assuming that our theory proves no falsehoods.

On the other hand, if $T$ proves that $M$ doesn't halt, then effectively it will have proved that it is itself consistent, and that is impossible according to the second Gödel-Rosser incompleteness theorem.

Since $M$ doesn't halt in any standard number of steps, and it can't be proved that it never halts, there must be a model of $T$ in which $M$ halts in a nonstandard number of steps. Therefore no standard upper bound for $\Sigma(|M|)$ is true in that model, and therefore $T$ can prove no such bound.

This is an expansion of the method in Henning Makholm's answer. We´ll work with ZFC here but any standard foundational theory would do. I will explain a proof that shows a different way to get the result about the unprovability of bounds of the Busy Beaver function. It shows that we can factor out the computability theory - we will not need to formalize computability theory within ZFC, we'll just work with computability theory in the metatheory. In that respect, this is different from Henning Makholm's answer.

Let $(\phi_n)$ be the standard enumeration of formulas of ZFC. Let $s(n)$ be the smallest Gödel number of a ZFC proof of $\phi_n$, if such a proof exists, or $0$, otherwise. Here the Gödel number of a proof, as usual, is just a single number that encodes the entire proof, under some effective coding scheme.

Let $P(m)$ be the maximum value of $\{s(0), s(1), \ldots, s(m)\}$. Thus $P(m)$ is an upper bound on the Gödel number of the shortest proof of $\phi_n$ whenever $n < m$ and $\phi_n$ is provable in ZFC. We will show that $P$ has a property analogous to the Busy beaver function, although $P$ is defined without any reference to computability.

We can define the function $P$ within ZFC, using the definitions above. So we can ask whether we can prove upper bounds on $P$. The answer is no:

Theorem. There is some $k$ such that ZFC does not prove any specific upper bound on $P(k)$.

The proof is as follows. Let $\Psi$ be the Gödel sentence of ZFC and choose $k$ such that $\Psi = \phi_k$. The key fact about the Gödel sentence is that it is not provable in ZFC, but ZFC does not prove that "$\Psi$ isn't provable in ZFC".

Suppose that ZFC proves that $P(k) < l$ for some fixed $l$. Take a model of ZFC that satisfies "$\Psi$ is provable". As usual, this model is necessarily nonstandard, and the "proof" of $\Psi$ within the model must be nonstandard. However, this model satisfies "The smallest Gödel number of a proof of $\Phi$ is less than $l$". Because $l$ is standard, this means that within the model there is a Gödel number $n$ of a proof of $\Psi$ which is bounded by a standard number, and thus $n$ is itself standard. This implies that $\Psi$ is provable in ZFC, which is a contradiction.

This immediately leads to a corollary about the Busy Beaver function. Let $B(n)$ be the least number of steps such that every Turing machine with fewer than $n$ states which halts at all halts in no more than $B(n)$ steps.

Theorem. There is some $r$ such that ZFC does not prove any specific upper bound for $B(r)$.

The proof is that, for each formula $\phi$ of ZFC, we can make a Turing machine that searches for a ZFC proof of $\phi$, and if it finds one it then runs enough steps so that its execution time is larger than the Gödel number of the proof it found, and then halts. Call this machine $T(\phi)$. Let $k$ be the number from the first theorem. We can find an $r$ such that every machine in $\{T(\phi_i) : i \leq k\}$ has no more than $r$ states. If we could prove an upper bound on $B(r)$, this would allow us to prove a bound on $P(k)$, which is impossible by the previous theorem.

Corollary. ZFC cannot prove an upper bound on $B(10\uparrow\uparrow 10)$.

Proof: If we let $\Psi$ be the Gödel sentence of ZFC, the machine $T(\Psi)$ has fewer than $10 \uparrow\uparrow 10$ states. It follows from the arguments in the previous proof that we cannot prove an upper bound in ZFC on $B(10\uparrow\uparrow 10)$.