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

Tag: z3 Author: achenjiang Date: 2013-04-12

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.

Z3 does not have decision procedures for integer arithmetic, or powers for that matter. Your use of simplification looks pretty neat to me to combine the features available.

Best Answer

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

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()

comments:

Wonderful, many thanks.