現在我們來討論定理機械化證明的複雜性問題，即難度問題。在這方麵人們特別感興趣的問題是，就定理證明而言，機器能在多大程度上代替人的腦力勞動。這就涉及了機器智能與人的智能的比較問題。
曾發表過一篇題為《智能與機器》的論文。他在這篇論文中提出了有名的“實驗”。這一試驗大致是這樣的：進行試驗的人與在其它房間裏的一個人和一台計算機進行問答。由進行試驗的人向另一個人和機器提出問題（例如某一行詩的作者是誰這樣的問題如果這個人辨別不出得到的回答是人給出的還是機器給出的，就算機器具有了人的智能。當時預測，在本世紀末就會有這樣的計算機。
對於這種看法，三十年來讚成的和反對的都有。關於讚成的意見，我們可以在70年代初在控製論學者中間搜集到的一些意見為例。
在1972年曾向英國和美國的六十三位控製論專家提出過下列的問題：你認為再過多久就能製成和成年人的智能相等的計算機他在調查表:列了一個答案。
我們認為，對於“何時能製成和成年人的智能相等的計算機?”這一問題是很難回答的。目前並非計算機在所有方麵都落在人的後麵。以處理信息的速度論，機器就遠遠超過了人。我們建議，對計算機和交互式的計算機係統進行比較，而研究下列的問題：是否能製成與交互式的計算係統能力相等的計算機？目前計算機的能力遠遠落後於交互式的計算機係統。但未來如何呢？這是我們要研究的問題。
在這裏我們要指出，上述問題是算機科學的中心問題之一，問題有密切聯係的。問題是問：在計算時間多項式有界的條件下，確定性的計算所能解決的問題是否和非確定性的計算所能解決的間問題一樣多這用所說的確定性的計算就是指依照通常的程序進行的計而非確定性的計算則是指依照非確定性程序進行的界。也可以這樣說：非確定性的計算是一種不斷地提高猜測，進行驗證，得到正確答案為的過程。從公理推定理的一種過程。則是在計算時間多項式有界的條件下，非確定性的計算機所能解決的大量問題的集合；而交互式計算係統就是一種能進行猜測的係統。
所以，交互式計算係統在計算時間多項式有界的條件下所能解決的大量問題的集合是包括在之中的。不難看出，通常的計算係統將和交互式計算具有相等的能力，於是就定理證明而言，交互式的計算係統將可以完全用通常的計算係統來代替。但目前絕大多數的有關科學工作者猜測。問題是一個難度非常大的問題。近年來有人猜測，對通常的集合論公理是獨立的，或者說是不可判定的(也就是說，從通常的集合論公理既不能推出也不能推出)。如果這一猜測成立，則表明對現有的數學而言，問題是無法解決的。
但不管上述理論問題的最終答案是什麼，定理的機械化證明是有廣闊的發展前景的，是有重大的理論與實踐意義的，這在目前已經是清楚的了。
這一證明技術有非形式的與形式的兩種。提出的方法叫做“歸納命題法”。這個方法的主要思想是，在一個程序和它的輸人謂詞與輸出謂詞給定後，通過證明一組關於這個程序中的若幹重要變量的命題之間存在著蘊涵關係，來證明這一程序的正確性。我們現在通過下麵一個簡單例子來說明這一方法是怎樣進行的。
用機器產生程序的想法也是在計算機產生後不久就有人提出過的，但認真開展研究是最近五六年的事。自動產生程序的方法之一是通過證明。例如設我們需要產生計算的值的程序。可以先存在的構造性證明。因為證明是構造性的，所以我們能夠從這一證明中提取計算的值的程序。這個方法的效率自然是低的。目前隻能產生一些簡單程序，離實際應用還很遙遠。
對自然語言的理解
近年來國外有些計算機研究中心一直在積極開展關於用自然語言來寫程序的研究，以及使計算機能“理解自然語言”的研究。在1971年曾構造了一個能和人用自然語言進行問答的係統。
在計算機機硬件和軟件設計正確性的驗證已成為受到重視的問題。軟件設計的正確性的驗證問題近年來有許多地方在從事研究）前這方鬧的研究大部分還處於理論階段，但已有了一些進展。硬件設計算機驗證的研究則剛剛開始。隨著計算機係統複雜件的增加.單憑著人的直觀來檢查一種設計是否有不合理之處，從而需要有形式驗證的方法。
近年來提出的“計算機設計語言”語言就是屬於這一類的.還有一則可以稱之為麵向功能的語言。這些語言主要是描述機器的輸人與輸出之間的關係的，所描述的僅限於硬件的輸入與輸出寄存器以及它們的狀態變遷，而對於實現這些狀態變遷的內部存貯兒則不加描述。語言就是屬於這後一類的。值得注意的是雖然語言現在一般認為是一種程序設計語言，而這一語的設計者最初卻是準備主要用這種語言來描述計算機硬件的。
目前利用硬件描述語言來從事係統設計的人還很少。這可能是由於至今還沒有一種為大多數計算機設計工作者所接受的語言；而且已有的語言也不夠豐富有力。
最近又出現了幾種新語言。1975年提出的一種寄存器傳送型語言就是其中之一。他們同時提出了一種對於用這種語言描述的機器設計進行驗證的方法，並且這是一種自動驗證係統。他們的方法的基本思想大致對於一種硬件的設計可有兩種描述，即①功能描述，②結構描述。硬件設計的驗證問題可陳述如下：給定一個硬件部件的功能描述和結構描述，檢查後者是否刻畫了和前者相同的輸人與輸出之間的關係。