關(guān)于作者
一個(gè)畢業(yè)于北京大學(xué)數(shù)學(xué)力學(xué)系，在中國科學(xué)院計(jì)算所、計(jì)算中心和網(wǎng)絡(luò)中心工作過，在澳大利亞科工組織DMS、香港浸會(huì)學(xué)院數(shù)學(xué)系和中國21世紀(jì)議程管理中心等處工作過，多次獲國家和中科院科技獎(jiǎng)并享受政府特殊津貼的退休老頭。現(xiàn)在在【中國科普博覽】網(wǎng)“科學(xué)新語林”欄目里開設(shè)一個(gè)《數(shù)學(xué)與計(jì)算機(jī)》的個(gè)人專欄，愿和愛好數(shù)學(xué)與計(jì)算機(jī)的各界網(wǎng)友和青少年朋友，談?wù)剬?duì)數(shù)學(xué)與計(jì)算機(jī)的看法、想法。
計(jì)算機(jī)證明（6）
張建中
2013年06月18日
10. 計(jì)算機(jī)證明的吳方法
“吳方法”的基本思想，首先借助坐標(biāo)系，把定理的假設(shè)與求證部分用一些代數(shù)關(guān)系式表示出來，即“幾何問題代數(shù)化”，然后再把表示代數(shù)關(guān)系的多項(xiàng)式做適當(dāng)處理，即把終結(jié)多項(xiàng)式中的坐標(biāo)逐個(gè)消去，當(dāng)消去的結(jié)果為零時(shí)，定理也就得到了證明。
幾何問題代數(shù)化是幾何問題機(jī)械化的第一步，為此需要引進(jìn)數(shù)系，建立坐標(biāo)系，把幾何命題圖中的各種關(guān)系利用代數(shù)方程描述出來。在適當(dāng)選取坐標(biāo)系后，如果幾何定理的假設(shè)條件可表示為一組代數(shù)方程[H]：f1=0，f2=0，…，fr=0，而幾何定理的結(jié)論由代數(shù)方程C：g=0所刻畫，這里f1,f2,…,fr和g都是變?cè)獂1,x2,…,xn的多項(xiàng)式，那么幾何定理的機(jī)械化證明就歸結(jié)為如下問題：機(jī)械化問題構(gòu)造并提供一種確定的、機(jī)械的算法，使得依此算法進(jìn)行有限步之后即可判定，在若干附加條件之下，結(jié)論C是否可由假設(shè)[H]推出，即是否可由f1=0，f2=0，…，fr=0推出g=0。
由此可見，實(shí)現(xiàn)數(shù)學(xué)定理機(jī)械化證明的關(guān)鍵，在于必須對(duì)表示定理假設(shè)的多項(xiàng)式組[H]的零點(diǎn)集給出構(gòu)造性的描述,以便區(qū)分多項(xiàng)式組[H]的零點(diǎn)集,從而可以確定在多項(xiàng)式組[H]零點(diǎn)集的哪部分之中,能夠保證多項(xiàng)式g=0。吳文俊消元法（吳方法）恰恰完成了這項(xiàng)任務(wù)。因此，吳方法是定理計(jì)算機(jī)證明原理的理論基礎(chǔ)，定理計(jì)算機(jī)證明的機(jī)械化原理的建立是吳方法的成功運(yùn)用。
吳文俊原理設(shè)數(shù)學(xué)定理的假設(shè)條件由多項(xiàng)式方程組[H]＝0表示，定理的結(jié)論由多項(xiàng)式方程g=0表示。并設(shè)CS＝{A1,A2,….,Ak}為多項(xiàng)式方程組[H]的特征列。如果多項(xiàng)式g對(duì)[H]的特征列CS的余式R=0,則在條件Ii≠0（i=1,2,…,k）之下,可從[H]=0推出g=0。
條件Ii≠0（i=1,2,…,k），稱為數(shù)學(xué)定理成立的非退化條件。這組非退化條件是在計(jì)算特征列過程中自動(dòng)產(chǎn)生的。非退化條件這一概念的發(fā)現(xiàn)，是吳文俊在數(shù)學(xué)機(jī)械化證明領(lǐng)域的突出貢獻(xiàn)。這一概念的引進(jìn)，實(shí)現(xiàn)了數(shù)學(xué)定理計(jì)算機(jī)證明的決定性突破。
11. 吳方法計(jì)算機(jī)證明一例
下面，以初等幾何定理“平行四邊形的對(duì)角線相互平分”為例，分三步說明如何用吳方法進(jìn)行幾何定理的計(jì)算機(jī)證明。
第一步：幾何問題代數(shù)化
①建立坐標(biāo)系，選好命題諸元
建如上圖所示的坐標(biāo)系：取點(diǎn)A、B、C、D為平行四邊形的四個(gè)頂點(diǎn)，且選點(diǎn)A為坐標(biāo)系的原點(diǎn)，線AB在x軸上，E為對(duì)角線AC和BD的交點(diǎn)；它們的坐標(biāo)分別取為A(0,0)，B(u1,0),C(u2,u3),D(x1,u3),E(x2,x3)，其中u1,u2,u3為自由變?cè)?，x1,x2,x3為約束變?cè)?。為保證平行四邊形ABCD不退化，要求 u1≠0、u3≠0；為保證AB∥DC，點(diǎn)A、B的第二個(gè)坐標(biāo)同為零，點(diǎn)C、D的第二個(gè)坐標(biāo)同為u3。
②把幾何命題圖中的各種關(guān)系利用代數(shù)方程描述出來
由線段AB = DC，得： ？1= u2-u1-x1= 0；
由B，E，D三點(diǎn)共線，得：？2 = x3(x1-u1)-u3(x2-u1)=0；
由A，E，C三點(diǎn)共線，得：？3 = x3u2-u3x2=0；
③待證明的結(jié)論為：
論為-300x34.png)
第二步：整序（三角化）
第三步：進(jìn)行逐步除法
這里的二、三兩步可用計(jì)算機(jī)完成。
大家看完這一證明后，可能感到此法比用兩角夾一邊證明 ABE和 CDE全等來證明“平行四邊形的對(duì)角線互相平分”復(fù)雜很多。只從此一例來看，的確如此。但當(dāng)從計(jì)算機(jī)證明來看問題，其意義就大不相同，而是開辟了數(shù)學(xué)定理證明的一個(gè)新方向，提供了對(duì)一大類幾何問題的證明方法，前景不可限量。
“吳方法”的基本思想，首先借助坐標(biāo)系，把定理的假設(shè)與求證部分用一些代數(shù)關(guān)系式表示出來，即“幾何問題代數(shù)化”，然后再把表示代數(shù)關(guān)系的多項(xiàng)式做適當(dāng)處理，即把終結(jié)多項(xiàng)式中的坐標(biāo)逐個(gè)消去，當(dāng)消去的結(jié)果為零時(shí)，定理也就得到了證明。
幾何問題代數(shù)化是幾何問題機(jī)械化的第一步，為此需要引進(jìn)數(shù)系，建立坐標(biāo)系，把幾何命題圖中的各種關(guān)系利用代數(shù)方程描述出來。在適當(dāng)選取坐標(biāo)系后，如果幾何定理的假設(shè)條件可表示為一組代數(shù)方程[H]：f1=0，f2=0，…，fr=0，而幾何定理的結(jié)論由代數(shù)方程C：g=0所刻畫，這里f1,f2,…,fr和g都是變?cè)獂1,x2,…,xn的多項(xiàng)式，那么幾何定理的機(jī)械化證明就歸結(jié)為如下問題：機(jī)械化問題構(gòu)造并提供一種確定的、機(jī)械的算法，使得依此算法進(jìn)行有限步之后即可判定，在若干附加條件之下，結(jié)論C是否可由假設(shè)[H]推出，即是否可由f1=0，f2=0，…，fr=0推出g=0。
由此可見，實(shí)現(xiàn)數(shù)學(xué)定理機(jī)械化證明的關(guān)鍵，在于必須對(duì)表示定理假設(shè)的多項(xiàng)式組[H]的零點(diǎn)集給出構(gòu)造性的描述,以便區(qū)分多項(xiàng)式組[H]的零點(diǎn)集,從而可以確定在多項(xiàng)式組[H]零點(diǎn)集的哪部分之中,能夠保證多項(xiàng)式g=0。吳文俊消元法（吳方法）恰恰完成了這項(xiàng)任務(wù)。因此，吳方法是定理計(jì)算機(jī)證明原理的理論基礎(chǔ)，定理計(jì)算機(jī)證明的機(jī)械化原理的建立是吳方法的成功運(yùn)用。
吳文俊原理設(shè)數(shù)學(xué)定理的假設(shè)條件由多項(xiàng)式方程組[H]＝0表示，定理的結(jié)論由多項(xiàng)式方程g=0表示。并設(shè)CS＝{A1,A2,….,Ak}為多項(xiàng)式方程組[H]的特征列。如果多項(xiàng)式g對(duì)[H]的特征列CS的余式R=0,則在條件Ii≠0（i=1,2,…,k）之下,可從[H]=0推出g=0。
條件Ii≠0（i=1,2,…,k），稱為數(shù)學(xué)定理成立的非退化條件。這組非退化條件是在計(jì)算特征列過程中自動(dòng)產(chǎn)生的。非退化條件這一概念的發(fā)現(xiàn)，是吳文俊在數(shù)學(xué)機(jī)械化證明領(lǐng)域的突出貢獻(xiàn)。這一概念的引進(jìn)，實(shí)現(xiàn)了數(shù)學(xué)定理計(jì)算機(jī)證明的決定性突破。
11. 吳方法計(jì)算機(jī)證明一例
下面，以初等幾何定理“平行四邊形的對(duì)角線相互平分”為例，分三步說明如何用吳方法進(jìn)行幾何定理的計(jì)算機(jī)證明。
第一步：幾何問題代數(shù)化
①建立坐標(biāo)系，選好命題諸元
建如上圖所示的坐標(biāo)系：取點(diǎn)A、B、C、D為平行四邊形的四個(gè)頂點(diǎn)，且選點(diǎn)A為坐標(biāo)系的原點(diǎn)，線AB在x軸上，E為對(duì)角線AC和BD的交點(diǎn)；它們的坐標(biāo)分別取為A(0,0)，B(u1,0),C(u2,u3),D(x1,u3),E(x2,x3)，其中u1,u2,u3為自由變?cè)?，x1,x2,x3為約束變?cè)?。為保證平行四邊形ABCD不退化，要求 u1≠0、u3≠0；為保證AB∥DC，點(diǎn)A、B的第二個(gè)坐標(biāo)同為零，點(diǎn)C、D的第二個(gè)坐標(biāo)同為u3。
②把幾何命題圖中的各種關(guān)系利用代數(shù)方程描述出來
由線段AB = DC，得： ？1= u2-u1-x1= 0；
由B，E，D三點(diǎn)共線，得：？2 = x3(x1-u1)-u3(x2-u1)=0；
由A，E，C三點(diǎn)共線，得：？3 = x3u2-u3x2=0；
③待證明的結(jié)論為：
論為.png)
第二步：整序（三角化）
第三步：進(jìn)行逐步除法
這里的二、三兩步可用計(jì)算機(jī)完成。
大家看完這一證明后，可能感到此法比用兩角夾一邊證明 ABE和 CDE全等來證明“平行四邊形的對(duì)角線互相平分”復(fù)雜很多。只從此一例來看，的確如此。但當(dāng)從計(jì)算機(jī)證明來看問題，其意義就大不相同，而是開辟了數(shù)學(xué)定理證明的一個(gè)新方向，提供了對(duì)一大類幾何問題的證明方法，前景不可限量。