第5期 杨路，等：常用基本不等式的机器证明 ·379· 正实数，则 对于算术与几何平均不等式(1)的机器证明， a“T. 还可以采取多种其他不同的策略，例如，容易知道， n n 日 算术与几何平均不等式(1)等价于如下的Jacobsthal 不等式[]： 显然，仅需对n个正实数a1,a2,…,an,证明如 (Ha>0,b>0,n≥1)(n-1)a"+b"≥ 下的算术与几何平均不等式： na"-1b. (8) “Ta, (1) 事实上，只需在式(5)中令￥=片，即可得到式(5) 与式(8)的等价性.式(8)对于n=1的情形是显然 即可直接证明几何与调和平均不等式，因为1,1 a1'a2 成立的，用数学归纳法完成式(8)的证明，只需引进 …,1皆为正实数，利用式(1)有 新变元s、t,执行BOTTEMA的xprove指令： an xprove(n*s*a+tb>= (n+1)*s*a*b,[(n-1)*s*a+t>=n*s*b]); ≥ (2) 屏幕几乎立即提示“The inequalitity holds'”. n 对于几何与调和平均不等式(3)，也可仿照上 将式(2)取倒数即得 述过程给出其机器证明方法，当然，直接利用算术与 VΠ4≥ n (3) 几何平均不等式(1)证明几何与调和平均不等式 (3)的过程也是非常简单的 如果考虑如下的算术与调和平均不等式： 下面给出式(1)的证明.容易验证式(1)在n= 1时成立.按照数学归纳法，假设式(1)成立，则需要 ≥n ∑”1 (9) 证明 n N+I 2k=1 dx T 类似上面的讨论，引进新变元A、B,执行BOTTEMA 的prove指令： 亦成立.由于式(1)成立，只需证 xprove((A +a)/(n +1)>= n3VT4+a≥(n+1)Va 4中 (n+1)/(B+1/a),[A/n>n/B]); 上式可以改写成： 即完成了式(9)的机器证明. I +1 l.2 Cauchy不等式的机器证明 n· a +1≥(n+1) (4) Cauchy不等式(Cauchy inequality）设x1,2, …,xn及y1,y2,…,y为2组实数数列，则 方便起见，作代换 正=心，式4)变为 +1 （∑)2≤∑∑元 an+l nx+1+1≥(n+1)x”. 该不等式的机器证明实现参见文献[1,23]，文献 (5) [23]基于QEPCAD,而文献[1]是基于BOTTEMA 现在，仅需证明式(5)对任意正数x和任意正整数n 成立即可.仍用数学归纳法，记式(5)为中，显然1 的.下面采用文献[1]的方法，记中n是如下公式： 成立.为证 (∑tw)-∑a∑ti≤0， 中n→中n+1, (6) 容易验证中1和中2成立.按照数学归纳法，需要证明 这时引进新的变元「，考虑命题： 中→0n+1: (10) (Vr>0,x>0,n≥1)nrx+1≥(n+1)r→ 这时引进新的变元r、s、t、xy,考虑命题： (n+1)rx2+1≥(n+2)rx. (7) （HT,s,t,x,y）r2≤st→ 如果式(7)为真，那么式(6)当然就为真，因为可以 (r+y)2≤(s+x2)(t+y2). (11) 令T代表x”,由于r、x、n全都是非负，因此可以执行 如果式(11)为真，那么式(10)当然就为真，因为可 BOTTEMA的xprove指令： 以令T、s、t、xy分别代表∑t=xy、∑t=1x、∑=1yi、 xprove((n +1)**1>= x+1y+…但式(11)和式(10)显然并不等价，事实 (n+2)*r*x,[n*T*x+1>=(n+1)*r]); 上，如果对实变量T、s、、x、y不附加任何其他条件的 屏幕几乎立即提示“The inequalitity holds”.这即完 话，命题式(11)是不成立的. 成了算术几何平均不等式的证明. 注意，式(11)是一个实量词消去问题，因而