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. – Daniel Lichtblau Jun 14 '19 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 Mar 30 '20 at 22:58
• @Jose: Nice catch! I've included your correction... which shortened the proof, by the way. – ShyPerson Mar 31 '20 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. – user64494 Mar 31 '20 at 8:52
• @user64494: Thanks for your clarifying comment. I've attempted to incorporate your suggestions. – ShyPerson Mar 31 '20 at 17:40