Background: Math undergrad, but complete layman in computer science
I recently asked this question on CS stackexchange. I hope I am interpreting the answers correctly:
Suppose we make a program to check that every even number greater than $2$ is the sum of two primes and run. All we have to do is run it for a certain, finite ammount of time; if a counterexample is found in that time, the conjecture is false. If no counterexample is found in that time, then the program will never halt so therefore the conjecture is true. Therefore there is an upper bound for the first possible counterexample.
My question is, how is this upper bound encoded mathematically in the Goldbach conjecture? Does this mean that any math problem can be answered by brute force in a finite ammount of time? I am still in shock; all my life I've been told that if you have a statement about infinitely many numbers, you will never be able to conclude that it is true by just plugging in more and more numbers; but apparently this is possible.
To me it's unbelivable that the upper bound for the smallest counterexample depends on our ability to encode the problem in a program.
EDIT: Reformulation suggested by user1952009 in the comments:
"What happens if someone had (for every nn) an upper bound for B(n)B(n). He can solve the halting problem and every number theory conjecture, so what ?"
This is much less deep than you seem to think it is. In fact, it is trivial that there exists a number $n$ with the property that there exists a counterexample to Goldbach's conjecture $\leq n$ iff Goldbach's conjecture is false. Namely, if Goldbach conjecture's is true, let $n=0$, and if Goldbach conjecture's is false, let $n$ be the smallest counterexample. Since Goldbach conjecture's is either true or false, either way there exists such an $n$. We just can't explicitly say what this $n$ is (because we don't know whether the conjecture is true, and we don't know what the least counterexample is if it's false).
The exact same thing is going on with the $n$ obtained from the busy beaver function. The definition of the busy beaver function involves testing which Turing machines halt, asking how long the ones that do halt take to halt. So part of the definition of the busy beaver value that you use to obtain your upper bound involves asking whether the computation you described ever halts, and taking the number of steps it takes if it does. That is, the definition of the busy beaver value you are using as an upper bound is basically the same as the definition of $n$ I gave in the previous paragraph, except that instead of just testing Goldbach's conjecture you are testing every conjecture that can be tested by running a Turing machine with a certain number of states.
So, it's not so much that the busy beaver function is built into Goldbach's conjecture. Rather, Goldbach's conjecture is built into the definition of the busy beaver function, such that the upper bound you get is a useless tautology.
Here's an even sillier variant on what's going on here. I claim there exists a very simple computation which correctly answers whether Goldbach's conjecture is true. Namely, if Goldbach's conjecture is true, take the computation that just immediately outputs "true". And if Goldbach's conjecture is false, take the computation that just immediately outputs "false". Goldbach's conjecture is either true or false, so either way one of these computations works! (We just don't know which one...)