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


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]



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/
  • $\begingroup$ Welcome to Mathematica.SE! I suggest that: 1) You take the introductory Tour now! 2) When you see good questions and answers, vote them up by clicking the gray triangles, because the credibility of the system is based on the reputation gained by users sharing their knowledge. Also, please remember to accept the answer, if any, that solves your problem, by clicking the checkmark sign! 3) As you receive help, try to give it too, by answering questions in your area of expertise. $\endgroup$ – bbgodfrey May 5 '15 at 16:11

How about

 Exists[{a, b}, 
  Element[a, Integers] && 
   Element[b, Integers] && ! MemberQ[Divisors[b], a] && a^2/b^2 == 2]]
(* False *)
  • 1
    $\begingroup$ 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. $\endgroup$ – Pillsy May 5 '15 at 16:38
  • 3
    $\begingroup$ 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? $\endgroup$ – Atriya May 5 '15 at 23:00
  • $\begingroup$ What happens if you rearrange the last equality to a^2 = 2 b^2? $\endgroup$ – J. M. will be back soon May 6 '15 at 0:40
  • $\begingroup$ 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! $\endgroup$ – Atriya May 6 '15 at 15:19
  • 1
    $\begingroup$ True seems fine as {0, 0} satisfy all the conditions as written. $\endgroup$ – ilian May 7 '15 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.