4
$\begingroup$

In a question on Mathematics SE, a comment observes that Mathematica 14.3 reports non-solvability of (a relaxation of) the given problem

Is there an odd $a \neq 1$ s.t. $2^k + 1 | a^k - 1$ for all $k \geq 0$

via

 In: FindInstance[{Mod[a^k - 1, 2^k + 1] == 0, 
       OddQ[a]}, {a, k}, Integers]

Out: {}

However, solutions exist; $(a,k) = (7,1)$ is given in a responding comment.

Documentation states: "FindInstance[$expr$, $x_1$, $x_2$, $\dots$] gives results in the same form as Solve: {{$x_1 \rightarrow val_1$, $x_2 \rightarrow val_2$, $\dots$}} if an instance exists, and {} if it does not." And a plain reading indicates that the output "{}" from FindInstance asserts an (internal) proof of nonexistence of solutions.

Is the documentation misleading, or is the implementation of FindInstance incorrect?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ For the original question, we at least need to use ForAll[k, k>=0&&k ∈ Integers] etc.. $\endgroup$ Commented 20 hours ago
  • $\begingroup$ @cvgmt : Agreed. But I expected to get a $k=1$ solution if the other $k$s were "hard". To get the "no solutions are possible" output was surprising. $\endgroup$ Commented 12 hours ago

3 Answers 3

Reset to default
6
$\begingroup$

To complement Bob's answer (+1), evaluate OddQ[a] on its own and see that indeed there are no solutions to the system {Mod[a^k - 1, 2^k + 1] == 0, OddQ[a]}, which first evaluates to {Mod[a^k - 1, 2^k + 1] == 0, False}. There's no way to satisfy the second condition. The tricky thing in Mathematica is that the boolean functions ending in Q immediately evaluate to True or False whether the input is symbolic or numeric. OddQ[a] answers the question, "Is a an odd Integer right now?" If a is just a symbol, then the answer is no.

Furthermore, PowerMod[] and bounding the domain make things faster. If the solutions are very sparse, then bounding the domain probably won't help. If the solutions are not sparse at all, then brute force may be fastest.

FindInstance[{Mod[a^k - 1, 2^k + 1] == 0, Mod[a, 2] == 1, 
   1 < a < 1000, 1 < k < 30}, {a, k}, Integers, 3] // AbsoluteTiming
(*
{0.314344, {{a -> 779, k -> 2}, {a -> 757, k -> 5}, {a -> 901, k -> 10}}}
*)

FindInstance[{PowerMod[a, k, 2^k + 1] == 1, Mod[a, 2] == 1, 
   1 < a < 1000, 1 < k < 30}, {a, k}, Integers, 3] // AbsoluteTiming
(*
{0.11144, {{a -> 779, k -> 2}, {a -> 757, k -> 5}, {a -> 901, k -> 10}}}
*)

(sols = Replace[
     Position[PowerMod[Range[1, 1000, 2], #, 2^# + 1] & /@ Range@30, 
      1, {2}], {kk_Integer, aa_Integer} :> {a -> 2 aa - 1, k -> kk}, 
     1]) // Length // AbsoluteTiming
And @@ (Mod[a^k - 1, 2^k + 1] == 0 && Mod[a, 2] == 1 /. sols)
(*
{0.004864, 1048}  <-- over 1K solutions found
True              <-- all true  
*)

The unbounded problem is more difficult:

FindInstance[{Mod[a^k - 1, 2^k + 1] == 0, Mod[a, 2] == 1, 1 < a, 
   1 < k}, {a, k}, Integers, 3] // AbsoluteTiming

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

(*  {1.76712, FindInstance[…]}  *)
Improve this answer
$\endgroup$
8
$\begingroup$ 
$Version

(* "14.3.0 for Mac OS X ARM (64-bit) (July 8, 2025)" *)

Clear["Global`*"]

Instead of OddQ[a], use Mod[a, 2] == 1

sol = FindInstance[{Mod[a^k - 1, 2^k + 1] == 0, Mod[a, 2] == 1, #}, {a, k}, 
     Integers][[1]] & /@ {True, k > 0, k < 0, 10 > a > 1 && k > 0}

(* {{a -> 1, k -> 0}, {a -> 1, k -> 1}, {a -> -1, k -> -970}, {a -> 7, k -> 1}} *)

Verifying the solutions,

Mod[a^k - 1, 2^k + 1] == 0 && Mod[a, 2] == 1 /. sol

(* {True, True, True, True} *)
Improve this answer
$\endgroup$
5
$\begingroup$

This is not a correct use of FindInstance.

Your query

FindInstance[{Mod[a^k - 1, 2^k + 1] == 0, OddQ[a]}, {a, k}, Integers]

asks the system to decide a nonlinear modular condition with a symbolic exponent. This is outside the scope of its decision procedures, so {} here does not mean "no solutions exist", it just means no instance was found.

A better formulation makes the limitation explicit:

f[a_, k_] /; OddQ[a] := Mod[a^k - 1, 2^k + 1];
FindInstance[f[a, k] == 0, {a, k}, Integers]

which returns:

FindInstance::nsmet: The methods available to FindInstance are insufficient…

So the issue is neither the documentation nor correctness. The solver simply cannot decide this problem. And indeed, solutions exist, e.g. {a -> 7, k -> 1}.

Improve this answer
$\endgroup$
1
  • $\begingroup$ This suggests that the original formulation should produce "FindInstance::nsmet: The methods available to FindInstance are insufficient…", which is not the case. $\endgroup$ Commented 12 hours ago

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.