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 ?"