當我們這樣來理解形式化這一概念時，可以立即看出形式化對計算自動化是必要的。與形式係統這一概念有關的概念有下列這一組，如“語法係統”，“公理係統”，“數學係統”以及“邏輯係統”。一個語法係統永遠是形式的，但逆之不真，因為我們可以說形式的語言學，公理的和形式的之間的關係與此類似。
數學係統和邏輯係統則情形更複雜一些，根據數理哲學的一個流派即所創立的邏輯主義，數學可以還原為邏輯，而對於多數當代的數學家而言，邏輯（此處指數理邏輯）僅僅是數學的一支，無論數學或邏輯並不必然是形式的（但邏輯基本上是形式的，所以數理邏輯和形式邏輯是同義詞。
如所周知，在早期的集合論中，發現了邏輯這一事實說明，在形式化方法中是存在有“陷阱”的，並且本世紀30年代以來，邏輯學者已經發現，形式係統有內在局限性，因為發現了不完備的係統。在1930年，在一次數學會議上宣布了一個驚人的結果，這個結果說，對任何一種複雜到一定程度的形式係統而言，如果它是協調的，它就是不完備的，這就是的不完備性定理。
計算機科學有關，由於一切遞歸函或者說一切與遞歸函數對程序）都是在程序理論中可表示的，如果這種理論是協調的，它就是不完備的。至於說形式方法的“陷講”，也就是“邏輯悖論”，本世紀初發現的“悖論”之中最有名的一個是這個“悖論”說明了邏輯和集合論的有些基本假定是錯誤的，這一錯誤的假定就是那個“概括性法則此法則可陳述如下:
數學定理的機械化證明
定理的機械化證明的研究始於1956年，當時打進行了利用計算機來證明初等幾何的簡單定理的試驗。他用的是探索法。接著和50100等人進行了用機器證明邏輯演算的定理的試驗，他們用的也是探索法。他們研製的那個“邏輯學者”係統是一個探索性程序。
1965年提出7種稱作“分解法則”的方法，比過去的方法更為有效，依然沒有多大進展。70年代以來5有人用交互程序取得進展。證明了群論和集合論的定理。
近年在這方閻得到成果。他證明了初等幾何中的一些不甚簡單的定理，就效率而言他的方法比過去用的分解法等方法要優越得多。因為分解法等都是通用的證明算法而吳的方法都是專用算法，因之效率較高。最近他還找出了初等微分幾何中的定理機械化證明的方法。他的工作受到了國內外有關的科學工作者的重視。
還有，1976年在計算機的幫助下解決了著名的“四色問題”。“四色定理”在一百年前有過一個證明，但不久人們發現這個證明有錯誤（四條引理中有一條引理的證明不能成立廠人等人用分情形證明的方法證明了那一條引理，從而證明了這一定理。因此，應該說，這條定理的證明主要是人做出來的。計算機隻起了輔助作用。自然，也必須承認，計算機在這條定理的證明中起了關鍵的作用，因為八等人在證明過程中用去了一台高速計算機的1200小時的計算時間，而且直到目前，我們也還不知道，這條定理是否有較簡短的證明。
結果說明了計算機作為定理證明的輔助工具的巨大潛力，這表明了在數學的未來發展中，數學工作者可以將定理證明中能夠機械化的部分交給機器去做，而自己專門去從事創造性的工作，即提出新概念，創造新方法以及設計新的證明算法等等。
另外，在純數學方麵，近年來獲得了一些出人意料的結果，為定理的機械化證明展示了廣闊的前景。這就是由隻第十問題所引出的某些結果。
第十問題是：找出一種方法，使得對任一給定的整係數的“丟番圖方程”，人們能夠借助這一方法來判定這個方程是否有整數解。這個問題是在1900年國際數學會議上提出的二十三個問題中的一個。1950年後，在此問題的研究上取得了重要進展。在1970年終於解決了這一問題，這是一項否定的解決（即證明了不存在這樣一種算法但卻產生了一係列肯定的結果，其中有的可能在定理機械化證明方麵有應用。
如果第十問題有肯定的解決“丟番圖方程”是否有整數解），而且這一判定算法是實際可行的（即判定過程所需要的時間不是長得無法實現的廣則“哥德巴赫問題”以及其它許多著名的未解決的問題，都將迎刃而解，可惜事實並非如此。第十問題的解決是否定的，因之後者的難度是否比前者小我們現在還不知道。但在1976年猜測，對於一些“丟番圖方程”有可能找到使得它們沒有整數解的可判定的充分條件，從而有可能借助計算機來判定這些方程有無整數解。