# FindEquationalProof to prove divisor theorem

I'm trying to implement proofs of concepts for Equational Proofs on some basic number theory theorems.

One such example is:

"let a and b be positive integers and let d = gcd (a, b). If t divides both a and b, prove that t divides d."

Implemented in Mathematica-12 as

ClearAll["Global*"]
axioms = {d == GCD[a, b] && Mod[a, t] == 0 && Mod[b, t] == 0}
FindEquationalProof[ForAll[{d, t}, Mod[d, t] == 0], axioms]


Upon evaluation, Mathematica returns:

Failure["PropositionFalse", Association["MessageTemplate" ->
TemplateObject[{"The proposition could not be reduced to True."},
InsertionFunction -> TextString, CombinerFunction -> StringJoin],"MessageParameters" -> Association[]]]


I've tried including logic in the "axioms" object for the variables' status as integers, but I end up with mathematica telling me my axioms are improper.

Any insight to this would be appreciated, as I'm quite sure this theorem is in fact true.

• One insight might be that d must divide t but not necessarily vice versa. Commented Jun 14, 2019 at 17:30

This is more a draft answer to your question than a full answer. Two observations: first, while I'm hardly any expert on evaluation in Mathematica, Mathematica seems to try to evaluate the terms given to it as arguments in FindEquationalProof. So Mathematica probably crashed when presented with unbound variables. Second, FindEquationalProof requires a full statement of the axioms to be used in a proof; there are no background axioms that come in by default.

So here's a draft of an answer; a little more work would need to be done to include Mod. The GCD axioms came from this article on Wikipedia.

axiom1 = {ForAll[{a}, gcd[a, a] == a]}
axiom2 = {ForAll[{a, b}, gcd[a, b] == gcd[b, a]]}
axiom3 = {ForAll[{a, b, c}, gcd[a, gcd[b, c]] == gcd[gcd[a, b], c]]}
hyp1 = {d == gcd[a, b]}
hyp2 = {gcd[a, t] == t}
hyp3 = {gcd[b, t] == t}
axioms = Union[axiom1, axiom2, axiom3]
hypotheses = Union[hyp1, hyp2, hyp3]
FindEquationalProof[gcd[d, t] == t, Union[axioms, hypotheses]]
`
• Nice answer. Note that axiom1 should say gcd[a, a] == a.
– jose
Commented Mar 30, 2020 at 22:58
• @Jose: Nice catch! I've included your correction... which shortened the proof, by the way. Commented Mar 31, 2020 at 2:45
• +1. In fact, axioms 4,5, and 6 are not axioms, but the hypotheses of the theorem. I suggest hyp1, hyp 2, and hyp 3 would be exacter notations. Commented Mar 31, 2020 at 8:52
• @user64494: Thanks for your clarifying comment. I've attempted to incorporate your suggestions. Commented Mar 31, 2020 at 17:40