# When can FindInstance prove no solutions for a nonlinear Diophantine equation?

A few months ago, I thought of a marvelous proof that $a^3+b^3=2c^3$ has no nontrivial integer solutions in $\mathbb{N}$, but the margin of my cocktail napkin was too small to contain it. Now I've forgotten it, I'm working on something that needs that lemma, and trying to see if Mathematica can help.

At the time, I remember thinking that my postulate could be proven to be a consequence of Fermat's Last Theorem, the latter of which Mathematica apparently knows:

FindInstance[a^3 + b^3 == c^3 && 0 < a <= b, {a,b,c}, Integers]
(* {} *)


But it seems that Mathematica can't always identify even trivial corollaries (the only difference is the coefficient in $8c^3$):

FindInstance[a^3 + b^3 == 8 c^3 && 0 < a <= b, {a,b,c}, Integers]


FindInstance::nsmet: The methods available to FindInstance are insufficient to find the requested instances or prove they do not exist.

In the "Diophantine Polynomial Systems" tutorial, Wolfram says that they use a "variant of the modular sieve method", but this method seems to be a topic that neither MathWorld nor Wolfram|Alpha are prepared to straightforwardly describe.

Before I ask my library to find a copy of The Algorithmic Resolution of Diophantine Equations on interlibrary loan, can somebody briefly describe when FindInstance will prove that there's no solutions, vs. when it will give up and say "I don't know"?

• Mathematica also knows FindInstance[ a^n + b^n == c^n && 0 < a <= b && n > 2, {a, b, c, n}, Integers] – Bob Hanlon May 19 '18 at 13:26