Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5

Question

Using the following code:

n = Int('n')
s = Solver()
s.add(n >= 5)
s.add(Not( n**5 <= 5**n))
print s
print s.check()

we obtain the following output:

[n ≥ 5, ¬(n^5 ≤ 5^n)]
unknown

It is to say that Z3Py is not able to produce a direct proof.

Now using the code

n = Int('n')
prove(Implies(n >= 5, n**5 <= 5**n))

Z3Py also fails.

A posible indirect proof is as follows:

n = Int('n')
e, f = Ints('e f')
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True)
prove(Implies(And(e >=0, f >= 0), t >= 0))

and the output is:

proved

A proof using Isabelle + Maple is given at :Theorems and Algorithms: An Interface between Isabelle and Maple. Clemens Ballarin. Karsten Homann. Jacques Calmet.

Other possible indirect proof using Z3Py is as follows:

n = Int('n')
e, f = Ints('e f')
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True)
s = Solver()
s.add(e >= 0, f >= 0)
s.add(Not(t >= 0))
print s
print s.check()

and the output is:

[e ≥ 0,
f ≥ 0,
¬(7849 +
9145·f +
4090·f·f +
890·f·f·f +
95·f·f·f·f +
4·f·f·f·f·f +
5·e ≥
0)]
unsat

Please let me know if it is possible to have a more direct proof using Z3Py. Many thanks.

Answer 1

Z3 has very limited support for nonlinear integer arithmetic. See the following related post for more information:

• How does Z3 handle non-linear integer arithmetic?

Z3 has a complete solver (nlsat) for nonlinear real (polynomial) arithmetic. You can simplify your script by writing

n = Real('n')
e, f = Reals('e f')
prove(Implies(And(e >=0, f >= 0), -(5 + f + 1)**5 + ((5 + f)**5 + e)*5 >= 0))

Z3 uses nlsat in the problem above because it contains only real variables. We can also force Z3 to use nlsat even if the problem contains integer variables.

n = Int('n')
e, f = Ints('e f')
s = Tactic('qfnra-nlsat').solver()
s.add(e >= 0, f >= 0)
s.add(Not(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5 >= 0))
print s
print s.check()