張景中，彭翕成，鄒 宇

幾何機(jī)器明證引發(fā)的思考

張景中1，2，彭翕成1，鄒 宇2

（1．華中師范大學(xué) 國(guó)家數(shù)字化學(xué)習(xí)工程技術(shù)研究中心，湖北 武漢 430079；2．廣州大學(xué)計(jì)算科技研究院，廣東 廣州 510006）

時(shí)代發(fā)展要求教育資源智能化，而不是簡(jiǎn)單的“電子化”．智能解答能在教育領(lǐng)域得以應(yīng)用的基本要求是能被人理解接受，即有很好的可讀性．最新研究表明，人類的解答未必是最好的，計(jì)算機(jī)可能給出讓人驚訝的解答．計(jì)算機(jī)給出的解答甚至比題干還短，這看似“有悖”常識(shí)，但又引起思考，如何知識(shí)表示才能盡量簡(jiǎn)潔而又方便推理．知識(shí)的創(chuàng)新表示，要盡量符合信息時(shí)代的要求，同時(shí)也可能造成原有知識(shí)體系的重新定位．

人工智能；教育應(yīng)用；幾何定理；機(jī)器明證；知識(shí)表示和推理

1 教育智能化是時(shí)代發(fā)展的必然要求

2016年AlphaGo橫空出世，擊敗了人類圍棋世界冠軍，人機(jī)博弈舉世矚目，言必稱“人工智能”的時(shí)代已經(jīng)到來[1-4]．人工智能研究包含但不限于以下研究課題：自然語言理解、數(shù)據(jù)庫的智能檢索、專家咨詢系統(tǒng)、博弈、機(jī)器人學(xué)、自動(dòng)程序設(shè)計(jì)、定理證明等．這里研究的幾何定理機(jī)器證明屬于定理證明領(lǐng)域的分支，包括如何讓計(jì)算機(jī)自動(dòng)出題以及解答．

解題研究是數(shù)學(xué)教學(xué)中的重要組成部分．學(xué)習(xí)數(shù)學(xué)離不開解題．學(xué)生要通過解題練習(xí)來掌握數(shù)學(xué)知識(shí)，老師需要通過試題分析來幫助學(xué)生提高．師生們面對(duì)各種難題，不會(huì)做怎么辦？考試出題人壓力更大，總被要求出題要有新意．一年當(dāng)中，考試繁多，對(duì)題目需求量大，那么多的新題從何而來？

這些問題存在多年．對(duì)于出題人而言，雖絞盡腦汁創(chuàng)新，但由于受到習(xí)慣思維的約束，與已有試題“撞車”也是常事．與之相對(duì)的是，廣大師生（甚至包括家長(zhǎng)）為解不出題，又找不到答案而苦惱．因此近十年來，各種題庫網(wǎng)站（包括APP）如雨后春筍般冒出，如菁優(yōu)網(wǎng)、魔方格、猿題庫、學(xué)霸君、作業(yè)幫等，頗受歡迎．其中智能手機(jī)的普及和拍照搜題技術(shù)的發(fā)展在其中起了很大的推動(dòng)作用．只是題庫再大，畢竟有限．對(duì)題庫中沒有的題目，就無能為力了．所以，在線題庫相對(duì)紙質(zhì)版的題典，只是題量更大，搜索更便捷．在智能化方面，并沒有本質(zhì)提升．缺少智能性或智能化程度不高是現(xiàn)有教學(xué)資源的一大通病[5-6]．

因此，利用計(jì)算機(jī)來研究智能化地命題和解題，很有現(xiàn)實(shí)意義．計(jì)算機(jī)出題，可不受已有題目的干擾，容易創(chuàng)新．如同AlphaGo下棋，很多招法超出人的想象．計(jì)算機(jī)解題，則可與已有題庫網(wǎng)站形成互補(bǔ)．題庫網(wǎng)站主要解決題庫已有題目，而計(jì)算機(jī)解題系統(tǒng)可解決題庫中沒有的題目．對(duì)于題庫已有題目，計(jì)算機(jī)解答系統(tǒng)也可以生成解答，對(duì)照檢驗(yàn)，看原有解答是否正確，又可給學(xué)習(xí)者提供多種解答思路．這也為接下來的自動(dòng)批改打下基礎(chǔ)．

目前從宏觀上討論人工智能與教育應(yīng)用的文章已經(jīng)很多了，這里將分享作者最近從事幾何定理機(jī)器證明的一些思考．

2 機(jī)器證明可讀性是教育應(yīng)用的基本要求

人工智能發(fā)展幾十年，發(fā)表了海量的學(xué)術(shù)論文．發(fā)展到一定階段，需要總結(jié)思考．在一些學(xué)術(shù)會(huì)議上，有人提出：人從小學(xué)到中學(xué)，讀書12年，到了18歲成年時(shí)，要通過高考，那么目前的計(jì)算機(jī)能否通過高考？這需要通過實(shí)踐來檢驗(yàn)．

中國(guó)在2015年啟動(dòng)了一個(gè)有關(guān)類人答題的863項(xiàng)目，其中包括初等數(shù)學(xué)的類人答題，要求計(jì)算機(jī)給出能被高考閱卷人認(rèn)可的解答，解答所使用的方法和知識(shí)點(diǎn)必須在中小學(xué)課標(biāo)范圍之內(nèi)．2017年6月7日，國(guó)產(chǎn)高考機(jī)器人挑戰(zhàn)北京卷文科數(shù)學(xué)以及全國(guó)二卷文科數(shù)學(xué)的考試，分別用時(shí)22分鐘和10分鐘，得分為105分和100分．這是一個(gè)相當(dāng)不錯(cuò)的成績(jī)．這一成績(jī)的取得，與中國(guó)科研工作者長(zhǎng)期的努力是分不開的．

1959年，IBM公司的Gelernter（曾參加1956年的達(dá)特茅斯會(huì)議）等人提出了后推搜索法來解幾何題，這一研究是20世紀(jì)50年代人工智能領(lǐng)域代表性成果之一，大大激發(fā)了人們對(duì)定理機(jī)器證明的興趣，確立了其在人工智能研究領(lǐng)域中的重要地位．但直到1976年，機(jī)器解答幾何題還停留在很初級(jí)的階段，只能解決一些很簡(jiǎn)單的問題．

1977年，由于吳文俊先生創(chuàng)造性的工作，幾何定理機(jī)器證明取得了突破性進(jìn)展．吳方法能判定幾何命題的真假，但其推理常涉及多達(dá)數(shù)百項(xiàng)甚至上千項(xiàng)的多項(xiàng)式計(jì)算，過程繁瑣，人們難以理解這些多項(xiàng)式的幾何意義，或者說證明的可讀性不令人滿意，檢驗(yàn)起來困難．從學(xué)術(shù)上來說，吳方法在理論上立得住，實(shí)踐中也有章可循，甚至有些簡(jiǎn)單問題手算都可以完成．但從教育應(yīng)用而言，可讀性差嚴(yán)重影響推廣普及．

以吳方法為代表的代數(shù)方法大獲成功，人們自然希望乘勝追擊，對(duì)機(jī)器證明提出了更高的要求．在之后多次有關(guān)機(jī)器證明的國(guó)際學(xué)術(shù)會(huì)議上，都有人提出這樣的問題：能不能由計(jì)算機(jī)給出易于理解、易于檢驗(yàn)的證明，即所謂可讀的證明？

定理的證明應(yīng)該被同行檢驗(yàn)，這是學(xué)術(shù)慣例．當(dāng)年四色問題的機(jī)器證明不可讀，引發(fā)了一場(chǎng)哲學(xué)討論：什么才算一個(gè)數(shù)學(xué)證明？一般認(rèn)為是，立足于一系列公理，從概念、定義、已有定理出發(fā)，采用演繹推理，得到新的結(jié)論．證明一方面要說服自己，當(dāng)解答者理清思路，認(rèn)識(shí)從模糊到清晰，才可能得出一個(gè)推理正確的證明．證明同時(shí)也要說服他人．所以一個(gè)好的證明除了推理正確，簡(jiǎn)潔明了也很重要．畢竟其他人未必有足夠的時(shí)間和興趣來檢驗(yàn)?zāi)愕淖C明．因此有觀點(diǎn)認(rèn)為[7]，證明就是某一特定時(shí)間，被某一特殊群體接受的解釋．Thomas Tymoczko認(rèn)為[8]，數(shù)學(xué)證明應(yīng)該有說服力（convincing）、可檢驗(yàn)（surveyable）、形式化（formalizable）．用數(shù)學(xué)同行公認(rèn)的語言進(jìn)行表達(dá)，是為同行檢驗(yàn)提供基礎(chǔ)；而檢驗(yàn)的目的則是為了說服同行，得到學(xué)術(shù)共同體的認(rèn)可．如果證明不可檢驗(yàn)，形式化的工作白做，也不可能說服同行，因此可檢驗(yàn)非常重要[9]．

是否“易于理解、檢驗(yàn)”，是一個(gè)模糊概念，因人而異．?dāng)?shù)學(xué)水平高、知識(shí)面豐富的，當(dāng)然理解能力強(qiáng)．對(duì)于教育應(yīng)用而言，必須假定讀者對(duì)象為中學(xué)師生．

機(jī)器能否生成可讀證明？數(shù)理邏輯專家王浩先生認(rèn)為，機(jī)器證明本質(zhì)是用量的復(fù)雜來代替質(zhì)的困難．吳文俊先生進(jìn)一步指出，人作幾何題，可根據(jù)不同情形找尋不同的巧法，巧則巧矣，卻是一題一法；機(jī)器證明要用統(tǒng)一算法解決不同問題，解題過程不可能簡(jiǎn)捷．機(jī)器證明是用冗繁但有章可循的計(jì)算來代替簡(jiǎn)捷巧妙但法無定法的推演．

盡管已有權(quán)威的論斷，但仍然有研究者沒有放棄．1992年，張景中等[10]提出了面積消點(diǎn)法，實(shí)現(xiàn)了“可讀證明（readable proof）”．在當(dāng)時(shí)看來，人能讀懂的機(jī)器證明，是極好的了，能與人工證明媲美了．

葉征等[11]認(rèn)為，幾何定理常有圖形輔助，閱讀證明時(shí)需反復(fù)比對(duì)證明文本和文本所對(duì)圖形中的幾何元素．如判定三角形全等，首先要在圖形中找到這兩個(gè)三角形，然后判定這兩個(gè)三角形是否大致全等，之后再繼續(xù)．當(dāng)證明較長(zhǎng)，或幾何圖形變復(fù)雜，不管是人工證明，還是機(jī)器證明，即使所謂的可讀證明也會(huì)變得不易閱讀和理解．因此提出幾何定理可視證明（visually proof），希望采用計(jì)算機(jī)圖形動(dòng)畫等方式幫助理解，使得幾何證明變得直觀．實(shí)踐表明，這是一種有效的方式．

問題是，當(dāng)證明很長(zhǎng)時(shí)，即便每一步都有幾何意義，即便每一步都有動(dòng)畫輔助，讀者依然會(huì)感到吃力，難以堅(jiān)持讀下去．可見，可視證明有助于讀者理解證明，但治標(biāo)不治本．揚(yáng)湯止沸，不如釜底抽薪．只有改善證明本身，使其變得簡(jiǎn)短易懂，才可能根本解決．

楊路等[12]在攻克不等式機(jī)器證明這一難題時(shí)，提出了“明證（certificate）”這一目標(biāo)，即證明一旦給出，讀者無需太多專業(yè)知識(shí)，很容易就能判斷證明是否正確，甚至是一目了然的．明證都無需專家審稿，普通讀者就能檢驗(yàn)．

一個(gè)不等式，一旦寫成平方和的形式，其結(jié)論一目了然．那么，幾何問題能否也實(shí)現(xiàn)“明證”，一行搞定？

一方面來說，幾何問題實(shí)現(xiàn)明證，要比不等式容易．因?yàn)椴坏仁缴婕啊案叽巍?，且變量多．幾何題雖有時(shí)也涉及“高次”，但多數(shù)情況下是一次、二次；幾何題雖從未限定過點(diǎn)、線、圓的個(gè)數(shù)，但多數(shù)情況下個(gè)數(shù)都不太多．但從另外角度來說，幾何題要實(shí)現(xiàn)明證，又要比不等式難得多．因?yàn)椴坏仁剑ㄟ@里主要指代數(shù)不等式）本身就是代數(shù)關(guān)系式，具備轉(zhuǎn)化變形的基礎(chǔ)．而幾何題涉及的幾何關(guān)系，需要通過轉(zhuǎn)換成代數(shù)形式，才有可能列出希望的“一行等式”．也就是幾何題比不等式多了一道轉(zhuǎn)化手續(xù)．解析幾何雖能實(shí)現(xiàn)幾何、代數(shù)之間的轉(zhuǎn)化，但表示幾何關(guān)系和表示幾何關(guān)系之間的關(guān)系十分繁瑣．因此有必要研究新的幾何表示，使得能簡(jiǎn)潔明了表示幾何關(guān)系；又要找到一種比較簡(jiǎn)單的方法，將幾何關(guān)系之間連接起來．

3 信息時(shí)代促使知識(shí)表示的再創(chuàng)造

一個(gè)知識(shí)點(diǎn)，往往存在多種表述形式．知識(shí)在傳遞給學(xué)生的時(shí)候，很有必要進(jìn)行批判再加工．這里的批判，主要不是懷疑這些知識(shí)的正確性，而是檢查它在教育上的適用性．要用系統(tǒng)科學(xué)的觀點(diǎn)，聯(lián)系前后左右的教學(xué)，聯(lián)系學(xué)生的心理特征與年齡特征，看一看，問一問，哪種反映方式較優(yōu)？能不能找到更優(yōu)或最優(yōu)的反映方式．

學(xué)習(xí)幾何，可選歐氏幾何，或解析幾何，或向量幾何，或質(zhì)點(diǎn)幾何，甚至可以創(chuàng)造新的幾何體系．哪種方案能更快更好地完成這一階段數(shù)學(xué)教育的任務(wù)呢？這需要仔細(xì)考察．在信息時(shí)代，還需要考慮該體系是否能被計(jì)算機(jī)簡(jiǎn)單地形式化處理．

以中點(diǎn)為例加以說明．怎么表示點(diǎn)是線段的中點(diǎn)？方法很多．

文字描述：點(diǎn)是線段的中點(diǎn)．

圖形描述（圖1）：

圖1

歐氏幾何描述：=．但不要漏掉：、、共線，否則只能說明點(diǎn)在線段的中垂線上．

中位線定理：

重心定理：

圖2

四邊形是平行四邊形的充要條件是：

．

等式簡(jiǎn)單變形，能得到新的幾何性質(zhì)，說明這一體系易于擴(kuò)展，生成新的知識(shí)．就是從這樣平凡之處著手，建立了點(diǎn)幾何體系[13-18]，并實(shí)現(xiàn)了多種基于點(diǎn)幾何的自動(dòng)推理算法，其中以點(diǎn)幾何恒等式算法尤為漂亮．

從知識(shí)工程[19]的角度來看，知識(shí)獲取和知識(shí)表示是從人類已有的知識(shí)源進(jìn)行抽取總結(jié)，并轉(zhuǎn)化成形式化的知識(shí)，便于用于問題求解．所謂形式化，是指利用計(jì)算機(jī)能接受并進(jìn)行處理的符號(hào)和方式來表示人類知識(shí)．符號(hào)表示是指用符號(hào)和符號(hào)結(jié)構(gòu)來表示各種概念和概念之間的關(guān)系．知識(shí)表示的選擇應(yīng)滿足：① 充分表達(dá)領(lǐng)域知識(shí)；② 有利于運(yùn)用知識(shí)進(jìn)行推理，有利于提高搜索速度及推理效率；③ 便于知識(shí)的維護(hù)和管理；④ 便于理解和實(shí)現(xiàn)．

建構(gòu)一種新的幾何體系，雖是為教育的目的，但若與計(jì)算機(jī)處理知識(shí)的方式吻合，則更加符合現(xiàn)代化教育的需求．在實(shí)現(xiàn)點(diǎn)幾何解答系統(tǒng)的過程中發(fā)現(xiàn)，點(diǎn)幾何體系的建立，符合知識(shí)工程的要求．而超過千例的計(jì)算機(jī)解題實(shí)踐更是表明，點(diǎn)幾何不僅符合數(shù)學(xué)直觀，能更方便地表達(dá)基本幾何事實(shí)，而且有助于幾何推理的簡(jiǎn)捷化．下面僅舉兩例說明．

圖3

證法1：

[0]：點(diǎn)、、、共圓

[1]：∠=∠(0)

[2]：是平行四邊形

[3]：∥(2)

[4]：∠=∠(3)

[5]：∠=∠(1 4)

[6]：點(diǎn)、、、共圓

[7]：∠=∠(6)

[8]：△∽△(5 7)

[9]：/=/(8)

[10]：∠=∠(0)

[11]：∠=∠(3)

[12]：∠=∠(10 11)

[13]：∠=∠(0)

[14]：△∽△(12 13)

[15]：/=/(14)

[16]：/=/(9 15)

例2 如圖4，△的邊為定長(zhǎng)，若邊的中線為定長(zhǎng)，試求頂點(diǎn)的軌跡．

圖4

4 幾何定理明證引發(fā)的思考

思考1：人類的證明是最好的么？

在AlphaGo的對(duì)戰(zhàn)中，人類千百年來積累的千錘百煉的定式一次次被推翻．AlphaGo也走出了人類公認(rèn)為壞棋的招法，但最終效果卻很好．棋手們長(zhǎng)期形成的圍棋觀被顛覆，需要重新思考：什么是好棋，什么是壞棋？

目前研究的機(jī)器解答，大多有一個(gè)定語，叫類人解答．也就是希望機(jī)器和人生成的解答盡可能類似，甚至是能混淆．這一方面是很早之前圖靈測(cè)試的期待，另一方面也是教育應(yīng)用的需要．問題是，人類解法也是多樣的，有平凡無奇的俗解，也有構(gòu)思奇特的巧解，甚至還有妙不可言的神仙手，如同天外飛仙，超出常人所想．

人類解法之中，有高有低，長(zhǎng)期以來人工智能專家追求的是計(jì)算機(jī)模仿生成人類的一般解法，因?yàn)樘茁坊?，方便操作．智能解答領(lǐng)域，能否像AlphaGo那樣，生成人類感到驚奇的解法呢．最新的研究表明，這是可能做到的．人給出的證明未必完美，機(jī)器證明可能超過人，給出更漂亮的解答．基于點(diǎn)幾何恒等式算法完成的例題解答有著很好的可讀性，因此具備出版并應(yīng)用于中學(xué)教育的可能．目前已與兩家出版社達(dá)成出版意向．華東師范大學(xué)出版社出版《點(diǎn)幾何解題》，主要介紹點(diǎn)幾何在解數(shù)學(xué)競(jìng)賽題方面的應(yīng)用．科學(xué)出版社出版《點(diǎn)幾何》，主要介紹點(diǎn)幾何的教育價(jià)值和教育應(yīng)用，以及自動(dòng)推理算法介紹，并輔以翔實(shí)案例說明．這兩本書里的題目，大部分來自人工收集，少部分由計(jì)算機(jī)自動(dòng)生成，解答主要由機(jī)器完成，人只在其中增加少量連詞和分析，使得讀起來更加順暢．計(jì)算機(jī)生成對(duì)聯(lián)、詩歌早有先例，此次生成幾何題集，在教育應(yīng)用中效果如何，拭目以待．

思考2：解答能否比題干短？如何表示知識(shí)是最簡(jiǎn)短的？

已有數(shù)學(xué)家證明，有些定理即使最短的證明也會(huì)很長(zhǎng)很長(zhǎng)．那么對(duì)于一般的初等幾何問題，證明最短能短到什么程度，能否短到與題干一樣長(zhǎng)，甚至更短？從“常識(shí)”來說，題干由若干條件和結(jié)論組成，條件看起來是零散的，條件之間存在隱藏的邏輯關(guān)系，而解答正是要把這些隱藏的邏輯關(guān)系找出來，隱藏關(guān)系顯現(xiàn)化的過程常常需要引入其它定理來說明，這樣才能將零散的條件（每個(gè)條件至少要用一次）串成一個(gè)完整的邏輯鏈，完成證明．這“必然”使得證明比題干要長(zhǎng)，甚至有的要長(zhǎng)幾倍，甚至十幾倍．一個(gè)兩三行的幾何題，證明花費(fèi)一兩頁的，并不少見．這真的是必然的嗎？

最近的研究表明，只要采取一種比較簡(jiǎn)潔而幾何意義豐富的知識(shí)表示形式，以及找到一種簡(jiǎn)單的推理方式，是可以做到解答比題干還短的．推而廣之，如何使得知識(shí)表示簡(jiǎn)單而意義豐富，推理簡(jiǎn)明容易實(shí)現(xiàn)，效率高且易于理解，這是一項(xiàng)很有研究意義又任重道遠(yuǎn)的工作．若能成功，即使是某一領(lǐng)域的部分成功，也能使得現(xiàn)有的推理體系大大簡(jiǎn)化，人們對(duì)事物之間關(guān)系看得更加清楚，大大減輕教與學(xué)的負(fù)擔(dān)．

思考3：新的知識(shí)表示方式，可能造成原有的知識(shí)體系重新定位．

近幾十年來，為了適應(yīng)信息時(shí)代的需要，世界各國(guó)的中學(xué)數(shù)學(xué)教材都做了相應(yīng)的改變，主要表現(xiàn)在對(duì)傳統(tǒng)的初等數(shù)學(xué)進(jìn)行了改造，滲透現(xiàn)代數(shù)學(xué)思想和方法．20世紀(jì)60年代，以新數(shù)學(xué)運(yùn)動(dòng)為代表的教育改革運(yùn)動(dòng)，喊出了“歐幾里得滾蛋”“打倒歐家店”的口號(hào)．英國(guó)一位教授認(rèn)為[20]：“這幾十年來，學(xué)生沒有學(xué)系統(tǒng)的平面幾何，英國(guó)并沒有出現(xiàn)科學(xué)人才危機(jī)，可見學(xué)不學(xué)歐氏幾何無關(guān)緊要．”歐氏幾何當(dāng)然有其學(xué)習(xí)價(jià)值．只是信息時(shí)代需要學(xué)習(xí)的內(nèi)容比以前大大增加了，而課時(shí)有限，如何進(jìn)一步精簡(jiǎn)綜合學(xué)習(xí)內(nèi)容，值得研究．

歐氏幾何自《幾何原本》算起，已有兩千多年．學(xué)習(xí)的難點(diǎn)，是構(gòu)造千變?nèi)f化的輔助線，使得圖形中出現(xiàn)全等或相似圖形．讓學(xué)生掌握輔助線的添加，需要花費(fèi)大量時(shí)間，但對(duì)進(jìn)一步數(shù)學(xué)學(xué)習(xí)的用處卻并不明顯．而最新的點(diǎn)幾何恒等式解題研究，其實(shí)質(zhì)是將幾何關(guān)系用向量形式表示，然后判斷條件和結(jié)論之間是否“線性相關(guān)”．也就是表面研究的是初等幾何，實(shí)際滲透的是高等代數(shù)的思想，為高等數(shù)學(xué)的學(xué)習(xí)打下基礎(chǔ)．采用新的知識(shí)表示，會(huì)使得原來看似不相關(guān)的知識(shí)體系變得連通起來，對(duì)原來的知識(shí)體系的價(jià)值也要重新定位評(píng)估．在信息化高速發(fā)展的今天，知識(shí)體系的改造盡量符合知識(shí)工程的需求也是大勢(shì)所趨．

[1] TURING A M. Computing machinery and intelligence [J]. Mind, 1950, 59 (236): 433-460.

[2] 吳砥，饒景陽，王美倩．智能教育：人工智能時(shí)代的教育變革[J]．人工智能，2019（3）：119-124．

[3] 馬玉慧，柏茂林，周政．智慧教育時(shí)代我國(guó)人工智能教育應(yīng)用的發(fā)展路徑探究——美國(guó)《規(guī)劃未來，迎接人工智能時(shí)代》報(bào)告解讀及啟示[J]．電化教育研究，2017，38（3）：125-130．

[4] 宋靈青，許林．人工智能教育應(yīng)用的邏輯起點(diǎn)與邊界——以知識(shí)學(xué)習(xí)為例[J]．中國(guó)電化教育，2019（6）：14-20．

[5] 張景中，李傳中．自動(dòng)推理與教育軟件智能平臺(tái)[J]．廣州大學(xué)學(xué)報(bào)（綜合版），2001，15（2）：1-6．

[6] 張景中．自動(dòng)推理與教育技術(shù)的結(jié)合[J]．中國(guó)青年科技，2001（8）：26-28．

[7] BALACHEFF N. Processus de preuves et situations de validation [J]. Educational Studies, 1987, 18 (2): 147-176.

[8] TYMOCZKO T. The four-color problem and its philosophical significance [J]. The Journal of Philosophy, 1979, 76 (2): 57-83．

[9] 張曉貴．對(duì)數(shù)學(xué)證明的審查與數(shù)學(xué)可謬性[J]．科學(xué)技術(shù)哲學(xué)研究，2018（4）：58-62．

[10] ?CHOU S C, GAO X S, ZHANG J Z. Machine proofs in geometry [M]. Singapore: World Scientific, 1994: 155.

[11] ?YE Z, CHOU S C, GAO X S. Visually dynamic presentation of proofs in plane geometry [J]. Journal of Automated Reasoning, 2010, 45 (3): 213-241.

[12] 楊路，夏壁燦．不等式機(jī)器證明與自動(dòng)發(fā)現(xiàn)[M]．北京：科學(xué)出版社，2008：152．

[13] 張景中．點(diǎn)幾何綱要[J]．高等數(shù)學(xué)研究，2018（1）：1-8．

[14] ?ZHANG J Z, PENG X C, CHEN M. Self-evident automated proving based on point geometry from the perspective of Wu’s method identity [J]. Journal of Systems Science & Complexity, 2019, 32 (1): 78-94.

[15] 張景中，彭翕成．點(diǎn)幾何的教育價(jià)值[J]．?dāng)?shù)學(xué)通報(bào)，2019，58（2）：1-4，12．

[16] 張景中，彭翕成．點(diǎn)幾何的解題應(yīng)用：計(jì)算篇[J]．?dāng)?shù)學(xué)通報(bào)，2019，58（3）：1-5，58．

[17] 彭翕成，張景中．點(diǎn)幾何的解題應(yīng)用：恒等式篇[J]．?dāng)?shù)學(xué)通報(bào)，2019，58（4）：11-15．

[18] 彭翕成，張景中．點(diǎn)幾何的解題應(yīng)用：復(fù)數(shù)恒等式篇[J]．?dāng)?shù)學(xué)通報(bào)，2019，58（5）：1-4．

[19] 楊炳儒．基于內(nèi)在認(rèn)知機(jī)理的知識(shí)發(fā)現(xiàn)理論[M]．北京：國(guó)防工業(yè)出版社，2009：37．

[20] 張奠宙．?dāng)?shù)學(xué)教育改革的十個(gè)問題[J]．教育學(xué)報(bào)，1993（3）：12-15．

Thinking Inspired by Geometric Machine Certificate

ZHANG Jing-zhong1, 2, PENG Xi-cheng1, ZOU Yu2

(1. National Engineering Research Center for E-Learning, Central China Normal University, Hubei Wuhan 430079, China;2. Institute of Computing Science and Technology, Guangzhou University, Guangdong Guangzhou 510006, China)

The development of times requires intelligent education resources, rather than simple “electronic”. The basic requirement that intelligent solutions can be applied in the field of education is that they can be understood and accepted by people, that is, they have good readability. Our latest research suggests that human solutions are not necessarily the best, and that computers may offer surprising solutions. The fact that a computer gives a solution even shorter than the stem of the problem seems “contrary” to common sense, but it also leads to the question of how to represent knowledge in such a way as to be as concise and convenient as possible for reasoning. The innovation representation of knowledge should conform to the requirements of the information age as far as possible, and at the same time may cause the repositioning of the original knowledge system.

artificial intelligence; educational application; geometric theorems; machine certificate; knowledge representation and reasoning

2019-12-20

國(guó)家自然科學(xué)基金項(xiàng)目——點(diǎn)幾何及其機(jī)器證明（11701118）

張景中（1936—），男，河南汝南人，中國(guó)科學(xué)院院士，研究員，博士生導(dǎo)師，主要從事機(jī)器證明、教育數(shù)學(xué)和教育技術(shù)研究．彭翕成為本文通訊作者．

G40-03

A

1004-9894（2020）01-0001-05

張景中，彭翕成，鄒宇．幾何機(jī)器明證引發(fā)的思考[J]．?dāng)?shù)學(xué)教育學(xué)報(bào)，2020，29（1）：1-5．

[責(zé)任編校：周學(xué)智、張楠]