計算機對數學發展的作用？

01-03

謝邀。

現在計算機在數學方面的主要應用還是比較傳統的驗算模式——數學家把某個問題約化成了只需要在有限種情形下進行驗證的問題——數學家眼裡的「有限」可不意味著「小」，整個宇宙的原子總數依然有限；然後數學家自己設計演算法、自己寫程序（或者和會編程的人合作寫程序），然後在電腦上跑，去驗證。典型例子包括——四色定理、球填充最高密度問題、以及最近那個什麼給整數染色使得任意勾股數組不同色的數據量大得不可想像的數論定理。另外我還知道馬里蘭大學有數學家用計算機做李群的某些無限維表示的分類問題——仍然是約化到有限情形——之前有大定理以非常抽象的方式給出了分類方法，然後他們花了整整10年時間寫程序實現，且項目主導人說他花費在數學推導和花在寫程序上的時間差不多長，充分說明拿計算機做驗算「看上去容易做起來難」。

另外也有人做機器證明之類的，比如幾何學、邏輯學定理的機器證明，但這些好像都是證的簡單的命題，我沒聽說過誰用機器證明證出open problem來的。

我個人覺得真正意義上的計算機證明，應該是計算機能夠自主思考、自主提出數學問題並自主證明或證偽，也就是像數學家那樣做數學，也就是強人工智慧。不過現在暫時還看不到希望——儘管Kontsevitch說他相信這種事情未來有可能實現。

前兩天看了一篇報道，再講到數論證明時，本來要證明在自然數成立，但證明非常困難，於是乎有人證明在足夠大的數中，定理成立。

接著有人給出這個足夠大數的上限。

當上限不是太大時，就不需要證明了，剩下的數用計算機枚舉驗證吧。

這樣就完成了自然數域的定理證明。

這可能就是作用之一吧

【果殼網專訪】哈洛德?賀歐夫各特：徹底證明弱哥德巴赫猜想

2013年5月13日，法國國家科學研究院和巴黎高等師範學院的數論領域的研究員哈洛德?賀歐夫各特，在線發表兩篇論文宣布徹底證明了弱哥德巴赫猜想。賀
歐夫各特在文章「Minor arcs for Goldbach"s problem」中，給出了指數和形式的一個新界。在文章「Major arcs
for Goldbach"s
theorem」中，賀歐夫各特綜合使用了哈迪-利特伍德-維諾格拉多夫圓法、篩法和指數和等傳統方法，把下界降低到了1

030

左右，賀歐夫各特的同事 David Platt 用計算機驗證在此之下的所有奇數都符合猜想，從而完成了弱哥德巴赫猜想的全部證明。

四色定理的證明

尋找完美正方形

離散數學

就像望遠鏡對天文學的作用，以及對撞機對物理學的作用。