证明是n^5 <= 5^N对于n> = 5

Question

使用以下代码：

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

我们得到以下输出：

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

这是说Z3Py无法提供直接证据。

现在使用的代码

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

Z3Py也会失败。

甲更多钞票间接证明如下：

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

并且输出是：定理和算法：

proved 

使用伊莎贝尔+枫树一个证明在给予Isabelle和之间的界面枫。 Clemens Ballarin。卡斯滕霍曼。雅克·卡尔梅特。使用Z3Py

其他可能间接证明如下：

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

，输出是：

[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 

请让我知道，如果有可能有使用Z3Py更直接的证据。非常感谢。

Answer 1

Z3对非线性整数算术的支持非常有限。请参阅以下相关职位的更多信息：

• How does Z3 handle non-linear integer arithmetic?

Z3具有非线性实（多项式）算术完整的求解器（nlsat）。您可以通过编写简化脚本

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在上述问题中使用nlsat，因为它仅包含实际变量。 即使问题包含整数变量，我们也可以强制Z3使用nlsat。

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