Is the Goldbach conjecture built into Wolfram?

Questions
1

From Wikipedia :
Goldbach’ s conjecture is one of the oldest and best -
known unsolved problems in number theory and all of mathematics .
It states that every even natural number greater than 2 is the sum of two prime numbers .
The conjecture has been shown to hold for all natural numbers less than 4*1018, but remains unproven despite considerable effort .

Resolve @ 
 ForAll[n, {EvenQ[n], IntegerQ[i], IntegerQ[j], n > 2}, 
  n == Prime[i] + Prime[j]]

True
2

Improved code:

Resolve @ 
 ForAll[n, {EvenQ[n], IntegerQ[i], IntegerQ[j], n > 2}, 
  Exists[{i, j}, n == Prime[i] + Prime[j]]]

True
3

You might want to check the values of the arguments. For instance, ForAll[n, False, False] evaluates to True. So does ForAll[n, False, x], because from the hypothesis False, any consequent follows.

You should find that each of EvenQ[n], IntegerQ[i], IntegerQ[j] evaluates to False, because like most *Q functions EvenQ[] and IntegerQ[] evaluate immediately to False if the argument is an expression explicitly does not satisfy the condition being tested as is. For instance, n has the head Symbol, not Integer.

4

Thanks for your input.

5

I would express the Goldbach conjecture this way:

Resolve@ForAll[n, {Element[n, Integers], n > 1},
  Exists[{i, j}, Element[i | j, PositiveIntegers],
   2 n == Prime[i] + Prime[j]]]
6

yes, it doesn’t evaluate, which is what you’d expect