繼給 GPT-4“代言”之后，Copilot 也被陶哲軒瘋狂安利。
他直言，在編程時(shí)，Copilot 能直接預(yù)測(cè)出他下一步要做什么。
有了 Copilot 之后，研究做起來(lái)也更方便了，陶哲軒也用它輔助自己完成了最新的研究成果。
陶哲軒說(shuō)，這次的論文中，有關(guān)這一部分的內(nèi)容其實(shí)只有一頁(yè)。
但具體完成這一頁(yè)紙的證明，他足足寫(xiě)了 200 多行代碼，用的還是新學(xué)的編程語(yǔ)言 Lean4。
而在陶哲軒公開(kāi)代碼的 GitHub 頁(yè)面上顯示，Copilot 將寫(xiě)代碼的速度提升了一半以上。
陶哲軒介紹，之所以選擇 Lean4 是看中了它的“重寫(xiě)策略”，也就是對(duì)一長(zhǎng)段表達(dá)式進(jìn)行針對(duì)性的局部替換。
舉個(gè)例子，假如定義了一個(gè)復(fù)雜的函數(shù) f (x)，當(dāng)我們想輸入 f (114514) 的表達(dá)式時(shí)，直接用代碼把 x“重寫(xiě)”成 114514 就可以了。
陶哲軒說(shuō)，這個(gè)特性相比于需要反復(fù)輸入公式的 LaTeX 簡(jiǎn)直不要太方便。
那么陶哲軒這次的“一頁(yè)紙證明”又給我們帶來(lái)了什么新成果呢？
一頁(yè)紙證明新不等式
這篇論文談?wù)摿擞嘘P(guān)麥克勞林不等式的問(wèn)題。
麥克勞林不等式是數(shù)學(xué)中一個(gè)經(jīng)典的不等式，它基于“非負(fù)實(shí)數(shù)的算數(shù)平均值大于等于幾何平均值”這一定律導(dǎo)出，可以表述為：
設(shè) y1…yn 為非負(fù)實(shí)數(shù)，對(duì) k=1…n，定義均值 Sk 為（分母為分子的項(xiàng)數(shù)）：
它作為具有根的 n 次多項(xiàng)式的歸一化系數(shù)而出現(xiàn)。
（記住這個(gè)式子，我們稱(chēng)它為式 1）
則麥克勞林不等式可以表示為：
其中，當(dāng)且僅當(dāng)所有 yi 相等時(shí)等號(hào)成立。
在微積分中，還有一個(gè)經(jīng)典的牛頓不等式：
對(duì)任意 1≤k<n，如果實(shí)變量 y1…yn 均為非負(fù)，牛頓不等式就可以簡(jiǎn)單地描述麥克勞林不等式了：
但如果不加上這個(gè)限制條件，即允許負(fù)數(shù)項(xiàng)的存在，用牛頓不等式就無(wú)法表示麥克勞林不等式了。
于是針對(duì)牛頓不等式中可能存在負(fù)數(shù)項(xiàng)的情況，陶哲軒提出了一組新的不等式變體：
對(duì)任意 r>0 且 1≤?≤n，必有式 2 或式 3 成立。
這便是陶哲軒這一頁(yè)紙所要證明的內(nèi)容，具體證明過(guò)程是這樣的：
不妨構(gòu)建一個(gè)關(guān)于復(fù)雜變量 z 的多項(xiàng)式 P (z)：
由前面的式 1 和三角不等式可得：
所以只需要建立下界：
對(duì) P (z) 取絕對(duì)值再取對(duì)數(shù)可得：
由于對(duì)任意實(shí)數(shù) t，t ? log (et+a) 呈凸性且 a>0，可以得到不等式：
當(dāng) a=r2，t=2log yj 時(shí)，可以得出：
以上就是陶哲軒給出的證明過(guò)程，但是，當(dāng)歸一化的 | Sn|=1 時(shí)，下式成立：
下一步：建立細(xì)化版本
除了這次提到的“一頁(yè)紙證明”，陶哲軒的這篇論文中還提出了另一項(xiàng)新的定理，即對(duì)任意 1 ≤ k ≤ ?≤ n.：
在博客文章中，陶哲軒透露，他的下一步計(jì)劃就是提出這一不等式的細(xì)化版本。
陶哲軒說(shuō)，證明的過(guò)程“就像練習(xí)一樣”會(huì)很簡(jiǎn)單，用微積分就能搞定。
不過(guò)，他也提到會(huì)有一個(gè)小困難，因?yàn)檫@部分論證過(guò)程使用到了漸進(jìn)符號(hào)。
新的結(jié)論具體怎樣，讓我們拭目以待。
One More Thing
陶哲軒可謂是 AI 工具的忠實(shí)粉絲，Copilot、GPT-4，還有一些其他輔助工具都受到過(guò)他的推薦。
這次，他還對(duì)大模型的發(fā)展提出了新的期待，希望有一天模型可以直接生成不等式變體。
論文地址：
https://arxiv.org/abs/2310.05328
參考鏈接：
https://mathstodon.xyz/@tao/111271244206606941
廣告聲明：文內(nèi)含有的對(duì)外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時(shí)間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。