**Motivation**

In this BBC video about infinity they mention Graham's number. In the second part, Graham mentions that "maybe no one will ever know what [the first] digit is". This made me think: Could it be possible to show that (under some assumptions about the speed of our computers) we can never determine the first digit?

In logic you have independence results like "We cannot decide if AC is true in ZF". But we cannot hope for this kind of result in this case, since we can easily program a computer to give us the answer. The problem is, that we don't have enough time to wait for the answer!

In complexity theory you prove things like "no program can solve all problems in this infinite set of problems, fast". But in this case you only have one problem, and it is easy to write a program, that gives you the answer. Just write a program that prints "1" another that prints "2" ... and a program that prints "9". Now you have a program that gives you the answer! The problem is, that you don't know which of the 9 programs that are correct.

**Questions**

**Edit:** I have now stated the questions differently. Before I asked about computer programs instead proofs.

- Could it be possible to show that any proof of what the first digit in Grahams numbers is, would have length at least $10^{100}$?
- Do there exist similar results? That is, do we know a decidable statement P and a proof that any proof or disproof of P must have length $10^{100}$.
- Or can we prove, that any proof that a proof or disproof of P must have length at least $n$, must itself have length at least $n$?

I think the answer to 3) is no, at least if all proofs are in the same system. Such a proof would prove that it should have length all least n for any n.

(Old Questions:

- Could it be possible to show that it would take a computer at least say $10^{100}$ steps to determine the first digit in Grahams number?
- Do there exist similar results? That is, do we know a decidable statement P and a proof that P cannot be decided in less that say $10^{100}$ steps.
- Or can we prove that we need at least $n$ steps to show that a decidable statement cannot be decided in less than $n$ steps?)

(I'm not sure I tagged correctly. Fell free to retag, or suggest better tags.)