繼給 GPT-4“代言”之后，Copilot 也被陶哲軒瘋狂安利。

他直言，在編程時，Copilot 能直接預測出他下一步要做什么。

有了 Copilot 之后，研究做起來也更方便了，陶哲軒也用它輔助自己完成了最新的研究成果。

陶哲軒說，這次的論文中，有關這一部分的內容其實只有一頁。

但具體完成這一頁紙的證明，他足足寫了 200 多行代碼，用的還是新學的編程語言 Lean4。

而在陶哲軒公開代碼的 GitHub 頁面上顯示，Copilot 將寫代碼的速度提升了一半以上。

陶哲軒介紹，之所以選擇 Lean4 是看中了它的“重寫策略”，也就是對一長段表達式進行針對性的局部替換。

舉個例子，假如定義了一個復雜的函數 f (x)，當我們想輸入 f (114514) 的表達式時，直接用代碼把 x“重寫”成 114514 就可以了。

陶哲軒說，這個特性相比于需要反復輸入公式的 LaTeX 簡直不要太方便。

那么陶哲軒這次的“一頁紙證明”又給我們帶來了什么新成果呢？

一頁紙證明新不等式

這篇論文談論了有關麥克勞林不等式的問題。

麥克勞林不等式是數學中一個經典的不等式，它基于“非負實數的算數平均值大于等于幾何平均值”這一定律導出，可以表述為：

設 y₁…y_n 為非負實數，對 k=1…n，定義均值 S_k 為（分母為分子的項數）：

它作為具有根的 n 次多項式的歸一化系數而出現。

（記住這個式子，我們稱它為式 1）

則麥克勞林不等式可以表示為：

其中，當且僅當所有 y_i 相等時等號成立。

在微積分中，還有一個經典的牛頓不等式：

對任意 1≤k<n，如果實變量 y1…y_n 均為非負，牛頓不等式就可以簡單地描述麥克勞林不等式了：

但如果不加上這個限制條件，即允許負數項的存在，用牛頓不等式就無法表示麥克勞林不等式了。

于是針對牛頓不等式中可能存在負數項的情況，陶哲軒提出了一組新的不等式變體：

對任意 r>0 且 1≤?≤n，必有式 2 或式 3 成立。

這便是陶哲軒這一頁紙所要證明的內容，具體證明過程是這樣的：

不妨構建一個關于復雜變量 z 的多項式 P (z)：

由前面的式 1 和三角不等式可得：

所以只需要建立下界：

對 P (z) 取絕對值再取對數可得：

由于對任意實數 t，t ? log (e^t+a) 呈凸性且 a>0，可以得到不等式：

當 a=r²，t=2log y_j 時，可以得出：

以上就是陶哲軒給出的證明過程，但是，當歸一化的 | S_n|=1 時，下式成立：

下一步：建立細化版本

除了這次提到的“一頁紙證明”，陶哲軒的這篇論文中還提出了另一項新的定理，即對任意 1 ≤ k ≤ ?≤ n.：

在博客文章中，陶哲軒透露，他的下一步計劃就是提出這一不等式的細化版本。

陶哲軒說，證明的過程“就像練習一樣”會很簡單，用微積分就能搞定。

不過，他也提到會有一個小困難，因為這部分論證過程使用到了漸進符號。

新的結論具體怎樣，讓我們拭目以待。

One More Thing

陶哲軒可謂是 AI 工具的忠實粉絲，Copilot、GPT-4，還有一些其他輔助工具都受到過他的推薦。

這次，他還對大模型的發展提出了新的期待，希望有一天模型可以直接生成不等式變體。

論文地址：

https://arxiv.org/abs/2310.05328

參考鏈接：

• https://mathstodon.xyz/@tao/111271244206606941

廣告聲明：文內含有的對外跳轉鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節省甄選時間，結果僅供參考，所有文章均包含本聲明。

總結

以上是生活随笔為你收集整理的陶哲轩疯狂安利 Copilot：它帮我完成了一页纸证明，甚至能猜出我后面的过程的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。