第5期 杨路，等：常用基本不等式的机器证明 ·381· 事实上，这就已经证明Chebyshev不等式对于均和 可在不到1s的时间内证明式(21)成立 单调的数列都是成立的，这已经在一定程度上推广 2)对于Bernoul山i不等式(21)中r取负整数的 了原来的Chebyshev不等式类型. 情形，此时式(21)在r=0时成立.记x=a+1,A= 对于上面通过BOTTEMA指令yprove证明的2 x“,归纳步骤变成证明 个命题，还有另一种较简单的，甚至可认为是机器明 (HA>0,x>0,n≥1)A≥1-n(x-1)→ 证(certificate)的方法，也是富有启发性的，在同 Ax1≥1-(n+1)*(x-1)). 类问题的机器证明中可能会有效.这里也简单介绍 使用BOTTEMA的xprove指令： 它的证明过程如下， prove(A/x>=1-(n+1)*(x-1), 命题1若s≤nt,nx≥r,y≥s,n≥1，则 [A>=1-n*(x-1)]); (r+x)(s+y）≤(n+1)(t+xy).(15) 同样可在不到18的时间内证明式(21)成立. 证明根据题设，不妨令 3)对于Bemoulli不等式(22)中r取1的情形， t=开+0，x=7+p,y=+q,(16) 此时式(22)在r=1时成立.记x=a+1,A=x,归 式中：0≥0，P≥0,9≥0，将式(16)代入 纳步骤变成证明 (n+1)(t+y）-(r+x)(s+y), 化简整理得 (A>0,>0,n>1)A<1+x-1)= wn pnq w. (17) 式(17)显然是非负的，于是式(15)成立，命题1得证 A<1+a*(-1). 类似地，可以证明如下的命题， 使用BOTTEMA的prove指令： 命题2若s≥nt,nx≥r,y≤s,n≥1，则 xprove(A<1+(1/(n+1))*(x*A-1), (r+x)(s+y)≥(n+1)(t+y).(18) [A<1+(1/n)*(x-1)]); 证明根据题设，不妨令 同样可在不到1s的时间内证明式(22)成立 =-=+py= -9,(19) ,m≥n时的 4)对于Bernoulli不等式(21)中r=m, n 式中：0≥0，p≥0,9≥0，将式(19)代人 情形，此时式(21)在r=1,即m=n时成立.固定n对m (r+x)(s+y)-(n+1)(t+xy), 应用归纳法，记x=a+1,A=x°，归纳步骤变成证明 化简整理，得 (VA>0,n≥1，m≥n)4≥1+%(A-1)→ wn png w. (20) 式(20)显然是非负的，于是式(18)成立，命题2得证 A1≥1+m+1*(A°-1)， n 命题1和命题2的证明根本无需B0 TTEMA,在 亦即 任何符号计算软件平台上都容易验证， 1.5 Bernoulli不等式的机器证明 (HA>0,n≥1，m≥n)A-1≥m(A"-1)→ Bernoulli不等式(Bernoulli inequality)】 设 41-1≥m+1*(A-1). a>-1,且r≥1或r≤0，则 n (1+a)'≥1+ar; (21) 而 若r的范围为(0,1)，则有 A-1=(A-10∑4 (1+a)'<1+ar (22) 于是，使用BOTTEMA的xprove指令： 成立 xprove(A-1)*(D+d)>=(A-1)*C*(m+1)/n, 1)Bernoull山i不等式(21)针对r取正整数情形的 [(A-1)*D>=(A-1)*C*m/n,m>=n, 机器证明实现参见文献[1].事实上，式(21)在r=1 (d-D/m)*(A-1)>=0]); 时成立.记x=a+1,A=x”,归纳步骤变成证明 即可在不足1s的时间内证明式(21)成立，因为可以令 (HA>0,x>0,n≥1)A≥1+n(x-1)→ C=t=4-D=∑A-1、d=Am.该条指令中的(d- A*x≥1+（n+1)*(x-1). D/m)*(A-1)>=0体现了数列{A,k=1,2,…}的单 使用BOTTEMA的xprove指令： 调性（或更准确地说，均和单调性）. xprove(A*x>=1+(n+1)*（x-1), [A>=1+n*(x-1)]): 5)类似地，对于Bernoulli不等式(22)中r= n