# Basic theorem proving in Mathematica?

Let's say we have the following:

p is prime
n > 1   (n is an integer)
p = nq (I.e. p is a multiple of n)


It can be proved that p = n.

I've seen that Mathematica has some basic theorem proving capabilities (see the theorem-proving tag) via functions like Reduce.

Can Mathematica prove the above claim? Pointers to external resources are welcome.

• $p=5$, $q=3$, $n=5/3$, $p$ is not equal $n$. Maybe you forgot something? – yarchik Aug 3 '19 at 19:43
• @yarchik Yes you're right, thank you! n is an integer. I've updated the post. – dharmatech Aug 3 '19 at 20:00
• Have a look at FindEquationalProof, though I think this may be harder than it looks. – Carl Lange Aug 3 '19 at 20:21

Mathematica does have such a thing, though it's unfortunately not as trivial as one would hope, as that:

FindEquationalProof cannot prove theorems involving arithmetic operators by default

As such, an example:

FindEquationalProof[a == b c, {a/c == b, c == 1}]

Failure["PropositionFalse",
Association["MessageTemplate" -> TemplateObject[{
"The proposition could not be reduced to True."}


If you read the docs under possible issues a solution to work around it.

FindEquationalProof[ForAll[x, f[4*x] == 4*f[x]], {ForAll[x, f[2*x] == 2*f[x]]}]
(*Same error as above*)

FindEquationalProof[ForAll[a, f[mult[4, x]] == mult[4, f[x]]], {ForAll[x, f[mult[2, x]] == mult[2, f[x]]], ForAll[{x, y, z}, mult[x, mult[y, z]] == mult[mult[x, y], z]], mult[2, 2] == 4}]


As such one would have to build in the logic of multiplying for your theorem to be found.