# 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.

This is something of a draft since I would have preferred to avoid writing the axioms for equality. But this seems blocked, since the documentation says "The statements stmt can consist of arbitrary logical combinations of predicates" where predicates don't seem to include == (equality). Comments and corrections welcome.

equalityAxioms =
{ForAll[{x}, eq[x, x]],
ForAll[{x, y}, Implies[eq[x, y], eq[y, x]]],
ForAll[{x, y, z}, Implies[And[eq[x, y], eq[y, z]], eq[x, z]]]}
multiplicationAxioms =
{ForAll[{a, b}, eq[m[a, b], m[b, a]]],
ForAll[{a, b, c}, eq[m[a, m[b, c]], m[m[a, b], c]]],
ForAll[{a}, eq[m[a, 1], a]]}
primalityAxiom = {Implies[prime[x],
ForAll[{a, b, x},
Implies[eq[x,
m[a, b]], (eq[a, x] && eq[b, 1]) || (eq[a, 1] && eq[b, x])]]]}
FindEquationalProof[(eq[p, n]),
Union[equalityAxioms,
primalityAxiom, {prime[p], ! (eq[n, 1]), eq[p, m[n, q]]}]]


Mathword page for relatively prime. For Wolfram Inc. are in the whole business world the problem of being relatively prime is of a major importance. Most cryptographic programs available nowadays work with big prime numbers.

Mr. Eric Weißstein named the built-in function:

CoPrimeQ

Since it is philosophically impossible to state that there is no occasion in the integer numbers for that the statement does not hold, but it is true that for all known integers the statement is valid.

There are several important mathematical functions related to that problem. Some state this is at the very foundations of Mathematica because automata are closely related to.

Mathematica use the principle of induction over the natural numbers, integers for enumerable primes. So the step is, if it is true for some certain natural numbering of the primes, it is true for the following one and that is allowed to be generalized for all finite integer, so it is getting probable that it is true for all.

Mathematica has a symbol infinity and can calculated limits but that does not work out in this case. All numbers involved can get bigger.

With newer versions of Mathematica there is the knowledge implemented:

Entity["FamousMathProblem", "CompositeNumberProblem"]


The output is available on Wolfram Alpha.

Further

composite prime number problem

The statement on Wolfram Alpha Pro ist

Row[{"The composite number problem is the determination of if for a \
given positive integer ", "N", "there exist positive integers ", "m",
" and ", "n", " such that ", Row[{"N == m n", "."}]}]

• Pay your attention to the difference between a theorem and its converse theorem (for example, see en.wikipedia.org/wiki/Theorem as a first reading). – user64494 Apr 10 '20 at 12:20