陶哲軒是公認(rèn)的數(shù)學(xué)天才，被譽(yù)為「數(shù)學(xué)神童」。他從小便展現(xiàn)出驚人的數(shù)學(xué)天賦，9 歲時就參加了美國數(shù)學(xué)奧林匹克，并獲得了金牌。他在數(shù)論、調(diào)和分析、偏微分方程等多個數(shù)學(xué)領(lǐng)域做出了重要貢獻(xiàn)，并獲得了菲爾茲獎， 這一獎項被視為數(shù)學(xué)界的最高榮譽(yù)，相當(dāng)于數(shù)學(xué)界的諾貝爾獎。 

最近，陶哲軒接受了《科學(xué)美國人》的采訪。在采訪中提出，未來數(shù)學(xué)家可以通過向類似 GPT 的 AI 解釋證明，AI 會將其形式化為 Lean 證明。這種助手型 AI 不僅能生成 LaTeX 文件，還能幫助提交論文，從而大幅提高數(shù)學(xué)家的工作效率和便利性。

他強(qiáng)調(diào)，AI 和自動化證明檢查器的引入將使得數(shù)學(xué)領(lǐng)域的合作方式發(fā)生根本性變化。通過將證明分解成小部分并由計算機(jī)驗證，數(shù)學(xué)家們可以在更大規(guī)模的項目上合作，而無需逐一驗證每個人的工作。

采訪文章地址：https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/

不過，這個討論也引起了一些爭議。有人認(rèn)為這會導(dǎo)致數(shù)學(xué)家變得懶惰和粗心，還可能導(dǎo)致數(shù)學(xué)證明的嚴(yán)謹(jǐn)性和創(chuàng)造力的下降。然而，陶哲軒解釋說，這種技術(shù)實際上是為了減輕數(shù)學(xué)家在證明過程中的繁瑣工作，讓他們可以專注于更具創(chuàng)造性和復(fù)雜性的任務(wù) 

盡管陶哲軒對 AI 在數(shù)學(xué)中的應(yīng)用持樂觀態(tài)度，他也承認(rèn)當(dāng)前技術(shù)尚未完全準(zhǔn)備好。目前的 AI 在處理數(shù)學(xué)家直覺和知識的方面還存在局限，很多數(shù)學(xué)知識并未在已發(fā)表的論文中捕獲，而是在對話和講座中傳授。

陶哲軒提供了一個復(fù)雜分析問題的示例，他通過與 ChatGPT 互動，解釋問題并生成了一個 LaTeX 文件。雖然目前的技術(shù)尚未實現(xiàn)完全形式化驗證，但這一示例展示了 AI 在協(xié)助數(shù)學(xué)證明方面的潛力。

陶哲軒昨日在博客中，對自己在采訪中的觀點(diǎn)進(jìn)行了進(jìn)一步解釋。

他談到自己在《科學(xué)美國人》中談到的觀點(diǎn)：我認(rèn)為在未來，我們將不再需要手動輸入證明，而是將它們講解給某種 GPT。這個 GPT 會在你講解的過程中嘗試將其形式化為 Lean 語言。如果一切都檢查無誤，GPT 會說：這是你的 LaTeX 數(shù)學(xué)論文；這是你的 Lean 證明，如果你愿意，我可以按下這個按鈕并將其提交給期刊。它將成為一個非常棒的助手。

這句話似乎引起了不同的反響，特別是被解讀為數(shù)學(xué)家會變得懶惰和草率。我認(rèn)為最好的方式來說明我的觀點(diǎn)是通過一個實際示例，這已經(jīng)是現(xiàn)有技術(shù)可以實現(xiàn)的。在我有一個中等難度的復(fù)分析問題。我在解釋了這個問題及其解決方案后，GPT 能夠提供解決方案的 LaTeX 文件。GPT 表現(xiàn)得相當(dāng)不錯，將我草擬的論證擴(kuò)展為一個相當(dāng)連貫且相對嚴(yán)謹(jǐn)?shù)耐暾C明。這還不是我在文章中設(shè)想的 100%，特別是缺少了保證正確性的嚴(yán)格 Lean 轉(zhuǎn)換，但希望能說明我在這句話中的想法。 

陶哲軒還補(bǔ)充說道， 采訪中提及按下按鈕將 GPT 生成的 LaTeX 文章提交給期刊的部分帶有玩笑性質(zhì)。但他認(rèn)為未來期刊會制定過濾器、標(biāo)簽要求和其他規(guī)則來管理部分或全部由 AI 生成的投稿。同時，他設(shè)想了新的文化規(guī)范，例如將 AI 生成并與 Lean 集成的互動形式的論文作為輔助版本，而人類撰寫的文本仍作為主要權(quán)威版本。 

也有網(wǎng)友表示，最大的難題其實是驗證證明的正確性。陶哲軒對此回應(yīng)道：

我認(rèn)為，采用新的工作流程實踐（例如那些在軟件工程或現(xiàn)有的形式化項目中已成為標(biāo)準(zhǔn)的流程）可以解決其中的許多問題。例如，應(yīng)該在開始證明過程之前先形式化結(jié)果的陳述，而不是在之后。我們還可以半自動或自動地對陳述進(jìn)行各種「合理性檢查 」或 「單元測試」，例如測試定理的瑣碎或非常簡單的情況，以及已知的更強(qiáng)版本定理的反例。(例如，在我的例子中，我加入了對該定理反例的驗證作為一種合理性檢查，盡管實際上目標(biāo)并不需要它）。

可見 AI 在數(shù)學(xué)領(lǐng)域的潛力巨大。在 AI 技術(shù)的輔助下，數(shù)學(xué)家的角色也將變得更加多樣化。未來可能出現(xiàn)的角色包括項目經(jīng)理、專門的 AI 培訓(xùn)師，以及將 AI 生成的證明轉(zhuǎn)化為人類可讀形式的專家。這將使數(shù)學(xué)研究更加類似于現(xiàn)代工業(yè)中的分工合作模式 。

如陶哲軒所說， AI 技術(shù)不僅能提高數(shù)學(xué)家的工作效率，還能通過形式化驗證保證證明的準(zhǔn)確性。這將為數(shù)學(xué)研究帶來革命性的變化，促使數(shù)學(xué)家在更短的時間內(nèi)取得更大的成果 。