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

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

他強調，AI 和自動化證明檢查器的引入將使得數學領域的合作方式發生根本性變化。通過將證明分解成小部分并由計算機驗證，數學家們可以在更大規模的項目上合作，而無需逐一驗證每個人的工作。

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

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

盡管陶哲軒對 AI 在數學中的應用持樂觀態度，他也承認當前技術尚未完全準備好。目前的 AI 在處理數學家直覺和知識的方面還存在局限，很多數學知識并未在已發表的論文中捕獲，而是在對話和講座中傳授。

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

陶哲軒昨日在博客中，對自己在采訪中的觀點進行了進一步解釋。

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

這句話似乎引起了不同的反響，特別是被解讀為數學家會變得懶惰和草率。我認為最好的方式來說明我的觀點是通過一個實際示例，這已經是現有技術可以實現的。在我有一個中等難度的復分析問題。我在解釋了這個問題及其解決方案后，GPT 能夠提供解決方案的 LaTeX 文件。GPT 表現得相當不錯，將我草擬的論證擴展為一個相當連貫且相對嚴謹的完整證明。這還不是我在文章中設想的 100%，特別是缺少了保證正確性的嚴格 Lean 轉換，但希望能說明我在這句話中的想法。 

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

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

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

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

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