關於是否會存在定理證明機，在理論上人們是有過不同的看法的。有些人認為不可能，如著名數學家龐加萊；而有些人卻覺得是可能的，並從理論上進行了論證，如著名的數理邏輯學家塔爾斯基。同時他還指出初等代數和初等幾何範圍的定理證明是可以實作機械化的。而在希爾伯特的【幾何基礎】中，也已經蘊涵了「萬理一證」的定理證明機械化思想，只是由於物質條件的不成熟而計人把他的這個重要思想給忽視了。然而，本世紀初數理邏輯的創立，以及40年代電子電腦的出現卻復興了這一想法，並且使之成為現實。
本世紀 50 年代，在這方面做出先驅性工作的是數理邏輯學家王浩教授，他僅用幾分鐘的時間就在電腦上證明了羅素和懷特海合著的【數學原理】中的300多條定理。這件事情為從事人工智能研究的人們著實興奮了一陣，但是這一切技術性的工作並沒有太多地引起數學界人士關於電腦對數學影響的重視，因為電腦所做的也就是人工所做的翻版。
然而70年代以後，電腦在數學中的套用卻給數學界帶來了未曾料想的影響，它使得人們開始重新思考數學的本質問題。 因為曾經困擾人們百年多的四色猜想在電腦上得到了證明，而且它的證明過程是人工無法檢驗的； 而以大自然中具有自相似形狀的物體為研究物件的碎形幾何，更是電腦下的產物。事實上，越來越多的數學問題的解決需要電腦的幫助，甚至是必須的。所有這些事實與人們從 19 世紀所接取過來的豐碩成果是這樣不同，於是自然地就引起了人們對數學哲學問題的思考和討論。
理論上的爭論
縱觀歷史的發展，人們想把推理機械化的思想很早以前就有，如柏拉圖、萊布尼茨、霍布斯、笛卡爾等等。而在近代，著名的德國數學大師希爾伯特在1899年出版的經典名著【幾何基礎】中，就已經指出了幾何定理可以不是逐一證明，而是一類定理可以用統一的方法一起證明。其大致的方向是從公理化出發，透過代數化而達到機械化。只是由於當時數學研究仍處於手工作坊時代，這個重要的機械化方向和意義沒有被數學家們及時地認識到。其實連希爾伯特自己也沒有明確地意識到。
希爾伯特
到了本世紀初，數理邏輯的發展為推理過程的機械化提供了基礎。無論命題演算還是謂詞演算都建立了公理系統，這就使得推理過程形式化。於是從一些很簡單明白的公理出發，使用一些很簡單的機械推理規則，便可一步一步地把人們日常使用的、乃至數學中所使用的極復雜的推理規則推匯出來。換句話說，人們日常使用的極復雜的推理規則，可以化歸為一些簡單的、機械的推理動作。最終的這些推理動作是這樣的簡單，以至於機械也可以實作，數理邏輯的成果讓人們認識到，可利用機器來部份地代替人類頭腦進行思維，正如可以利用機器來代替人類的體力勞動一樣。
這種對推理過程認識的深化，自然地就導致有些數理邏輯學家提出關於定理證明機的想法。即∶有可能制造出一種機器以代替人類思維，代替人類進行推理。但是也有人反對，最有代表性的如當時一代數學大師龐加萊就對這個想法大加責難，還帶有諷刺般地說：
現在已經有屠宰機器，當把牲畜趕到機器的一端時，機器便把這些牲畜宰殺成罐頭，從另一端輸送出來；現在有人竟然想制造一部機器，當把定理的前件送到機器的一端後，便可以把定理的結論從機器的另一端輸送出來（或者公理、定義送到一端後，各式各樣的定理便從另一端輸送出來），這種想法是註定不可能實作的。
龐加萊的看法絕不僅僅是他一個人特有的想法，實際上是代表了當時數學界流行的、占統治地位的思想。試想一想，在這種想法流行的時候，特別還是那麽有聲望的大人物所反對的想法，人們還會想方設法制造電子電腦去實作定理證明嗎？
然而隨著數理邏輯對推理過程本質研究的漸漸被認識，反對制造定理證明機的人們在日益減少，而支持的人卻越來越多。本世紀50年代，塔爾斯基首先從理論上證明了 ∶在初等幾何以及初等代數的定理證明是可以機械化的。 不過他給出的機械化方法過於繁復，在實踐中真正實作起來是相當困難的。正是因為這樣，所以他的結果給人以這樣一個感覺∶定理證明能機械化的設想是個例外，因為大部份初等幾何及初等代數以外的結果都是不能機械化的。另外，塔爾斯基還提出了制造證明機的設想。無疑這種理論上的闡明是重要的，就如圖靈從理論上證明電子數碼電腦是可能的一樣，它讓人覺得自己的實踐和試驗不是盲目的。
科技的進步為人們的這些設想提供著物質基礎，終於人們制造出了證明定理的機器。
五十年代中期，美國開始利用電腦進行證明數學定理的嘗試。
1959年，王浩用電腦證明了羅素和懷特海所著的【數學原理】這一經典著作中的300 多條定理，一共只用了9分鐘的機器時間。這件事在數學界（特別是數理邏輯界）引起了轟動。他所使用的方法就是羅素和懷特海的技術，因為在【數學原理】中有許多標準的技巧是可以很快地變為機械的手續。接著J.A.Robinson發展了並使之成為一種標準的方法。這個結果就導致許多人對定理機器證明的前途看好，甚至有人還在1958年做出預測說，在10年之內電腦將發現並證明一個重要的數學新定理。也有人設想，前人像皮亞諾、懷特海、羅素、希爾伯特以及圖靈等的夢想都將實作，然而事情的進展並沒有人們預想的那樣順利，不過隨著時間的推移，這些設想終究成為了現實。
首先是20世紀70年代， 美國的數學家阿佩爾和黑肯借助於電腦證明了著名的四色猜想，震動了數學界。 它標誌著電腦證明數學定理有著很好的前景。盡管如王浩先生的說法，四色猜想的證明是一種使用電腦的特例機證，但是它是一個由人沒有能夠解決的數學問題。而且它的證明又非傳統上的形式，於是就引起了人們繼數學基礎研究、希爾伯特探討數學證明之後的又一次對數學證明的思考： 什麽是數學證明？
而上世紀70年代，在國際上掀起的一股研究以"非"字當頭的科學中，由曼德布羅特創立的碎形幾何學，更是得力於電腦的強大功能。電腦在這裏並不是證明定理，而是幫助人們提出猜想，引發思考。我們當如何看待這門學科呢？有人認為它不是數學。但也有更多的人認為它是一門數學學科，特別是物理學家，因為碎形幾何正在成為研究大自然中許多復雜現象的有力工具。雙方爭執的焦點是"什麽是數學"這個基本的數學哲學問題。
四色猜想證明的歷史
1976年1月，困擾了無數智者100多年的四色猜想由人機合作終於獲得了解決。面對這一事實，有人帶著些驚喜、有人帶著些遺憾、也有人帶著些懷疑，畢竟它不是數學家們所希望的那種傳統演繹證明定理的方式。
四色問題
四色問題是一個屬於拓撲學的問題，它的粗略描述可以追溯到1840 年。當時數學家莫比烏斯在給學生的講課中提到。在平面上很容易指出四個區域，其中每兩個區域都有一個公共的邊界線，並要求學生證明： 在平面上決不可能指出五個區域都具有上述性質。 從這個論斷的證明中，可得出莫比烏斯假設∶ 平面或球面上的每張地圖都可以用四種顏色來著色。
明確提出四色問題的是倫敦大學學院畢業不久的學生弗朗塞斯·古斯裏（1852）。他在一封給他兄弟弗雷贅克的信中說∶
看來，每幅地圖都可以只用四種顏色著色，使得有共同邊界的國家著上不同的顏色。
這是原始四色問題的描述。由於他的兄弟無法解決，所以就這個問題的證明去請教他的老師——英國著名的數學家、邏輯學家德·摩根，據說德·摩根當天就寫了封信給當時正在英國三一學院執教的著名數學家、物理學家哈密頓。然而這兩位數學家實際上都沒有能夠解決這個看上去非常簡單的問題。
後來英國著名的數學家凱萊於1878年倫敦數學家會議上正式公布了這個問題。他呼籲與會者去解決這一問題。就這樣，和費馬大定理一樣，這個表面看似明易懂，其實很奇特的問題進入了數學家的圈子。從此受到了數學界人士的普遍重視以及數學愛好者們的興趣。以後，宣布證明了四色問題的聲明源源不斷，可是一經檢查，總是有或大或小的、難以彌補的缺陷。
在眾多聲稱證明了這一論斷的解答中，最值得一提的是1879年有一位名叫肯普的會員（同時也是律師）送出的一篇論文。凱萊和當時其他的一些數學家檢查後確定證明是正確的。誰知過了10年，也即在1890年，年僅 29歲的英國數學家希伍德在證明中卻發現了漏洞。這樣，四色猜想依然固我，沒有被解決。直到如今才借助於電腦給予解快。
肯普的證明是有錯誤，然而他的證明思路非常有價值。因為一方面 20 世紀的人們正是沿著他的證明思路，逐漸改進而借助於電腦最終解決了四色問題；另一方面，希伍德在肯普方法的基礎上還證明了"五色定理"，特別是對歐拉示性數為K時的曲面上的地圖著色數P_k給出了上界：
四色問題的解決
前面已經提及，肯普的證明有錯誤，但包含了許多天才的思想。
肯普是采用反證法證明四色猜想的，具體思路是∶ 如果有需要五種顏色的地圖，則此種地圖中必定有一個最小的，也就是在需要五種顏色的地圖中有一個區域數目是最少的（這種地圖稱為最小五色地圖）。於是只要證明這種最小的地圖是不存在的，問題就可以獲得解決。因為假如給定了這樣的一種地圖，最後總能夠對它進行"歸約"而找到一種更小的地圖，而這幅地圖也需要五種顏色。為此，肯普先把問題轉化為只研究一種所謂的正規地圖，在這種地圖中由有兩個鄰國、三個鄰國、四個鄰國及五個鄰國組成的一組構形是不可避免的，也即他需要證明總得有一個國家其鄰國數小於等於5。在這個條件下，肯普把上述論證又簡化成四條引理:
（1）每一地圖都含有五個或五個以下鄰域的區域；
（2）最小的五色地圖不可能含有恰好有兩個或恰好有三個鄰域的區域（因為如果那樣我們將能夠找到一個更小的需要五種顏色的地圖）；
（3）同樣地，這樣的地圖不可能含有恰好有四個鄰域的區域；
（4）這樣的地圖不可能含有恰好有五個鄰域的區域。
對這四種情況經過檢檢視是否有"可約構形"出現，如果都有，矛盾就出現了。肯普對於引理1）一3）證明得很成功，但是在4）上卻失敗了。
20世紀的數學家們從肯普跌倒的地方開始了艱難的跋涉。
首先是美國數學家伯克霍夫。1913年他在肯普的基礎上引進了一些新技巧，這促進了富蘭古連於1939年證明22國以下的地圖都可以用四色著色；1950年溫（Winn）又把22國改進為35國；再接著是1968年奧爾（他是唯一的一本關於四色問題專著的作者）把數目提高到39國；1975 年又報道，對 52 國以下的地圖四色猜想都成立。從時間上可以看出，四色問題解決的進展是極其地緩慢。其中一個一直難以解決的困難，是肯普證明中關於五個鄰國時可約構形的判斷問題。具體地說是如何把 4）中的情況分得足夠細。
在四色問題的解決之路上，數學家H.希什也做出了很大的貢獻。他從1936 年就開始對四色問題進行研究，且始終堅信四色問題可以透過尋找可約構形的不可避免組得到解決。到1950年他從不斷的試驗中猜測，如果把情況分細到可以證明的地步，則這個組裏的構形可能需要大約一萬多種情況才行。要對如此多的構形逐一證明，工作量之大是非人力所能完成的。恰逢電子電腦在計算速度、精確度等方面都得到了驚人的進展，希什敏銳地意識到，若把證明構形可約的方法形式化，在理論上有一部份是可以透過電腦解決的。於是他很快就試著利用人機結合去解決，這也是早期人工智能的一種嘗試。
最初他與其學生是圍繞著怎樣用電腦檢查圖形是否可約構形進行的。盡管希什曾猜測可能要分一萬種情況，可是誰也不知道是否真得需要有一萬種，況且即使是對一種不太復雜的情況，若要檢查也要用上百個小時，而對較復雜的情況，無論是在時間上，還是在儲存上，電腦都不能承受。
美國伊利諾斯大學的黑肯教授在總結以往各種證法後指出，如果運用現有的一切數學方法，不可能給出四色猜想一個傳統上的證明，而在還沒有一個更強有力的電腦之前，能否給出一個電腦證明也是沒有把握的。就在這樣的信念下，黑肯對希什的方法作了重要的改進，接著是與阿佩爾合作著手研究四色問題。兩人一方面從理論上繼續簡化問題，另一方面又利用電腦的試算和人機對話。從中獲得有益的啟示。後來二人連手設計了一個能做出特殊類別放電過程的電腦程式，並經過上機不斷地反復試驗、不斷地修改，特別是在電腦專家科克的參與下，最後終於在1976年1月6日，由三人找到了一個合適的可行程式，證得了可約構形的不可避免組。於是百年來讓人們苦苦思索的這個敘述簡單明了的四色猜想，在IBM360機上執行達1200多小時後得到了證明。他們是利用"窮舉檢驗"法分情況檢查的，當時一共分了1482種情況，經查證它們都是可約構形。
四色猜想的證明是如此的繁復，盡管在 1977 年的一次數值數學與電腦會議上，有人又官布了一個相對簡單的證明，可是也要用50機時。所以它不像數學中上其它問題的證明，獲得數學家們的一致贊揚，而是引起了許多的爭議。
爭議
從四色猜想的解決過程可以看到，它是眾多數學家合作的結晶，是對歷史上智者探索的完善。阿佩爾等人是采用組合語言編寫程式解決了四色問題、其程式之復雜到如今都還有人時不時地檢查出錯誤，雖然是不影響全域的；而且就目前的解決方法來看，其工作量之大是人力所永遠無法達到的。面對四色問題的這種復雜的、又是借助於電腦的證明，人們給以各種各樣的反應。正如國際上的數學家們所認為的，阿佩爾和黑肯等人的貢獻並不在於證明了四色問題，而在於借用電子電腦完成了這個至今人還沒有能夠解決的問題。但是，也有一些數學家反對四色猜想已經成為一個定理，於是自然地就引發一場爭論。這場爭論的焦點集中在電腦證明的可靠性和四色猜想的電腦證明是不是數學證明的問題。
關於機器證明的可靠性問題
反對四色定理的人認為∶如果一個定理不能用手工進行檢查，無法核實其證明是否可靠，就不能接受它是一個定理。電腦用了 1200個小時才證明了四色定理，這是用手工幾代人也無法檢查完的。事實上，在1961年，就有人聲稱借助於電腦找出了一個不可免完備集，其中的構形全是可約的（果然如此的話，四色猜想當然獲證）。但是，惠特尼和塔特卻各自獨立地發現，有一個構形的可約性被電腦誤算了，從而那個證明是錯誤的。事實上，自從黑肯和阿佩爾在 1976 年解決四色猜想之後，人們一直都在不斷地從證明中發現一些錯誤，慶幸的是這些錯誤都可以被修正而不影響證明的全域。但是誰也無法保證，有一天不會從中找出一個致命的錯誤；機器中的硬件或軟件的錯誤。這就是機器證明的可靠性問題。
但是，贊成四色猜想是一個定理的人卻認為∶
機器的可靠性主要是工程技術和物理學鑒定的事情，這是一門深奧的自然科學，它向我們保證，電腦的工作是可靠的，就象電子顯微鏡的工作是可靠的一樣。
美國著名數學家瑟斯頓在【數學的證明和進展】一文中談道：
實際上，一個可以運作的電腦程式，其正確性和完備性標準比起數學界關於可靠的證明的標準要高出幾個數量級。
關於四色猜想的電腦解決是不是數學證明的問題
不承認四色猜想的電腦解決是屬於數學證明的人認為，沒有一個數學家曾看到過四色猜想的證明，也沒有一個數學家看到過它的證明的證據，沒有數學家全面地驗證過四色猜想的證明。如著名蘇格蘭數學家波塞爾在其文章【切合實際的數學觀】一文中提到的：
如果這樣的一個問題（例如四色問題）利用某種聰明的新思想解決了，那是很了不起的。但是、如果解決的方法只是一個現存方法的反復使用，那就只能證明解決者的聰明罷了。如果解決的方法包括用電腦來證明特殊情況，那也是糟糕的，按我的觀點，這樣的解根本不屬於數學科學。
不加驗證地接受電腦給出的資訊，還不如接受另一個數學家的告誡。事實上，例行公事似的編制程式十分乏味，極可能造成程式的錯誤。如果讓部份論證隱藏在電腦的鐵盒中，我們就不可能得到所認為的證明中的實質東西——我們自己對問題的了解。
1988年的紐約時報上還刊登了這樣一篇文章：【沒人能檢驗的證明算是數學證明嗎？】。
贊成者認為，機器證明是有可靠性問題，但是，有的數學定理被數學家證明了，但過了幾十年，人們又發現其證明是錯誤的，這說明人工證明也有一個可靠性問題。所以只對機器證明提出可靠性問題是不公平的。
而另一方面，電子電腦正越來越多地介入到數學中的各個領域裏來。特別是近年在數學中的某些領域，有許多的問題如果不借助於大型的電腦，常常是無法解決的，如關於大數質性的檢驗、關於一個有限單純群的構造性的證明等問題。
總之，圍繞著四色猜想的電腦解決，人們提出了許多重大的問題∶技術上的和哲學上的。四色猜想的電腦證明之意義，決不僅僅在於一個歷時多年的難題的解決。就從目前的趨勢看，它很可能將成為數學發展史上一系列新思想的引子。碎形幾何的創立就是一個說明。
