可讀證明(readable proof)機器證明的基本概念.指能夠不花太多的時間和精力就可以被人理解和檢驗其正確性的證明.用傳統方法給出的幾何定理的證明是可讀的.而用機器證明的代數方法。
可讀證明(readable proof)機器證明的基本概念.指能夠不花太多的時間和精力就可以被人理解和檢驗其正確性的證明.用傳統方法給出的幾何定理的證明是可讀的.而用機器證明的代數方法，如吳方法、GB法或數值並行法來證明定理，由於過程中計算量一般較大，人們難以看明白並加以檢驗，所產生的證明不是可讀的.能不能用機械的方法產生可讀證明?自1960年以來，歐美一些學者開始研究這一重要問題，提出了各種構想.中國的吳方法成功後，這個問題引起了人們的更大關注.1992年5月，張景中等人給出了世界上第一個能自動產生幾何定理可讀證明的算法和通用程式.在微機上成功地產生了近千條非平凡的幾何定理的可讀證明，其中許多證明簡短而優美，這是機器證明的又一突破.機器生成可讀證明的研究在幾年間得到很大的發展.
