5
$\begingroup$

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.

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

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.

$\endgroup$

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.