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

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/

FullSimplify[
Exists[{a, b},
Element[a, Integers] &&
Element[b, Integers] && ! MemberQ[Divisors[b], a] && a^2/b^2 == 2]]
(* False *)
• It turns out the ! MemberQ[Divisors[b], a] clause is unnecessary; Mathematica will simplify the without it. The key change seems to be squaring both sides of the equation. May 5, 2015 at 16:38
• I am accepting this, and not the answers of @ilian and Pillsy for the following reason. The point of the question was not merely to find out if Mathematica can determine if root 2 is rational or not, since it common knowledge that it is not. Rather, I suspect that users including myself, would hope to use it to find the truth or falsity of complex statements, which might not have the form necessary to simply use the Element function, for example. Here, it is very troubling to me that the sides need to be squared in order to get a decision. In general, how would I know what to change? May 5, 2015 at 23:00
• What happens if you rearrange the last equality to a^2 == 2 b^2? May 6, 2015 at 0:40
• It just gave me True as a reply for FullSimplify[ Exists[{a, b}, Element[a, Integers] && Element[b, Integers] && ! MemberQ[Divisors[b], a] && a^2 == 2 *b^2] ]! This seems to be incorrect! May 6, 2015 at 15:19
• True seems fine as {0, 0} satisfy all the conditions as written. May 7, 2015 at 11:15

As far as obtaining a True/False answer:

Element[Sqrt[2], Rationals]

(* False *)

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.