# 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 at 17:30