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

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

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

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

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

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

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

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

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

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

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

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

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

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

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