2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ One insight might be that d must divide t but not necessarily vice versa. $\endgroup$ – Daniel Lichtblau Jun 14 at 17:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.