Proving (or at least 'being told by Mathematica') that Sqrt[2] is irrational?

Question

I realize that Mathematica is not specifically an automated theorem prover. However, this article:

http://www.wolfram.com/products/mathematica/newin6/content/EquationalTheoremProving/

Suggests that Mathematica 6 onwards can apparently prove certain theorems. Examples are provided of expressions being provided to FullSimplify, and it coming up with a True or False response, depending on whether the expression is True or False (presumably in some axiom system internal to it). The proof itself is not provided.

The documentation also mentions, that Mathematica 'knows' about Fermat's Last Theorem. Indeed, the example provided:

FullSimplify[x^n + y^n == z^n, Element[x | y | z | n, Integers] && n > 2 && x y z != 0]

Gives

False

as expected. I would usually formulate this as:

FullSimplify[Exists[{x, y, z, n}, x^n + y^n == z^n && Element[x | y | z | n, Integers] && n > 2 && x y z != 0]]

and indeed that does give the same result. Am I to conclude that Mathematica is 'proving' or at least 'calculating' the result somehow using proprietary heuristic rules? Or is this particular theorem, being a famous one, simply hard coded into it? The documentation seems to suggest this by saying that Mathematica 'knows' about the theorem.

Specifically, I tried to prove a simple result - the irrationality of the square root of 2:

FullSimplify[Exists[{a, b}, Element[a, Integers] && Element[b, Integers] && a/b == Sqrt[2]]]

but all Mathematica does is re-format the expression into Mathematical notation. It is apparently unable to 'prove' or otherwise obtain a True/False decision. Of course, False is expected.

Is this simply something Mathematica cannot, as of now, do, or am I doing something wrong (and there is indeed some way to prove the irrationality of Sqrt[2] in Mathematica)?

Just as a note:

1. Yes, I am aware of Theorema 2.0, but it seems incomplete and hardly documented as of now.
2. I am also aware of this blog post: http://blog.stephenwolfram.com/2014/08/computational-knowledge-and-the-future-of-pure-mathematics/

Answer 1

How about

FullSimplify[
 Exists[{a, b}, 
  Element[a, Integers] && 
   Element[b, Integers] && ! MemberQ[Divisors[b], a] && a^2/b^2 == 2]]
(* False *)

Answer 2

As far as obtaining a True/False answer:

Element[Sqrt[2], Rationals]

(* False *)

Answer 3

The quickest route here, from a syntactic standpoint, is to use Reduce, which allows you to request that the equation to be simplified by eliminating a set of variables, and to restrict those variables to a given domain, all at once:

In[1]:= Reduce[a^2/b^2 == 2, {a, b}, Integers]
Out[1]= False

As shown in Marius Ladegård Meyer's answer, you need to square both sides of the equation for this to work:

In[2]:= Reduce[a/b == Sqrt[2], {a, b}, Integers]
Out[2]= (a | b) ∈ Integers && 
         ((a <= -1 && b == a/Sqrt[2]) || (a >= 1 && b == a/Sqrt[2])) 

EDIT to add: I discovered some time after the fact that FullSimplify and even Simplify can do it with the additional assumption that $ b \ne 0 $ without the weird need to square things:

In[3]:= Simplify[a/b == Sqrt[2], {a, b} ∈ Integers && b != 0]
Out[3]= False

I've only tried this in Mathematica 10.2, so perhaps it didn't work in earlier versions.