陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程
关于麦克劳林不等式
克雷西 发自 凹非寺
量子位 | 公众号 QbitAI
继给GPT-4“代言”之后,Copilot也被陶哲轩疯狂安利。
他直言,在编程时,Copilot能直接预测出他下一步要做什么。
有了Copilot之后,研究做起来也更方便了,陶哲轩也用它辅助自己完成了最新的研究成果。
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/a25ec8e4d393d6e0b591c01ea9ba3387.png)
陶哲轩说,这次的论文中,有关这一部分的内容其实只有一页。
但具体完成这一页纸的证明,他足足写了200多行代码,用的还是新学的编程语言Lean4。
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/80207f57296c902db24e12fa43491f77.png)
而在陶哲轩公开代码的GitHub页面上显示,Copilot将写代码的速度提升了一半以上。
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/86343786c68c9bc0f7c88b79c4c721e4.png)
陶哲轩介绍,之所以选择Lean4是看中了它的“重写策略”,也就是对一长段表达式进行针对性的局部替换。
举个例子,假如定义了一个复杂的函数f(x),当我们想输入f(114514)的表达式时,直接用代码把x“重写”成114514就可以了。
陶哲轩说,这个特性相比于需要反复输入公式的LaTeX简直不要太方便。
那么陶哲轩这次的“一页纸证明”又给我们带来了什么新成果呢?
一页纸证明新不等式
这篇论文谈论了有关麦克劳林不等式的问题。
麦克劳林不等式是数学中一个经典的不等式,它基于“非负实数的算数平均值大于等于几何平均值”这一定律导出,可以表述为:
设y1…yn为非负实数,对k=1…n,定义均值Sk为(分母为分子的项数):
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/afafe4593f6010aeb7fe493d35cfc280.jpeg)
它作为具有根的 n 次多项式的归一化系数而出现。
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/9cea40f0b6a83f03e9180ba01767fff3.jpeg)
(记住这个式子,我们称它为式1)
则麦克劳林不等式可以表示为:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/5e3ef16b8e827cd93f9dcf04e45a56a4.jpeg)
其中,当且仅当所有yi相等时等号成立。
在微积分中,还有一个经典的牛顿不等式:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/1b401cc423751be351df3b23999a7fe7.jpeg)
对任意1≤k<n,如果实变量y1…yn均为非负,牛顿不等式就可以简单地描述麦克劳林不等式了:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/2a4220556956a34bd842b5d095cd1c85.jpeg)
但如果不加上这个限制条件,即允许负数项的存在,用牛顿不等式就无法表示麦克劳林不等式了。
于是针对牛顿不等式中可能存在负数项的情况,陶哲轩提出了一组新的不等式变体:
对任意r>0且1≤ℓ≤n,必有式2或式3成立。
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/926c27db24ffae36c2c7d05f8aca16cd.jpeg)
这便是陶哲轩这一页纸所要证明的内容,具体证明过程是这样的:
不妨构建一个关于复杂变量z的多项式P(z):
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/e09cf84f00ff822b5499bc8580281c9c.jpeg)
由前面的式1和三角不等式可得:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/eafa380dfb2063a36f71ff4ad78718ea.jpeg)
所以只需要建立下界:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/cbaa7d4f6bcc11f0fae9a6bae2266d98.jpeg)
对P(z)取绝对值再取对数可得:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/17986e5455ed5cd79722e2192f699321.jpeg)
由于对任意实数t,t ↦ log(et+a)呈凸性且a>0,可以得到不等式:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/8fab814d727ef5a07114b33814a34d10.jpeg)
当a=r2,t=2log yj时,可以得出:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/1a4ec1ad83fdad98f998f66df9bf8a58.jpeg)
以上就是陶哲轩给出的证明过程,但是,当归一化的|Sn|=1时,下式成立:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/3dacc93fdf466d71dedd8d1878cb1d87.jpeg)
下一步:建立细化版本
除了这次提到的“一页纸证明”,陶哲轩的这篇论文中还提出了另一项新的定理,即对任意 1 ≤ k ≤ ℓ≤ n.:
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/6bbe6677ddc641441e1e274c8b91b4a9.jpeg)
在博客文章中,陶哲轩透露,他的下一步计划就是提出这一不等式的细化版本。
陶哲轩说,证明的过程“就像练习一样”会很简单,用微积分就能搞定。
不过,他也提到会有一个小困难,因为这部分论证过程使用到了渐进符号。
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/0e164c46c76d66406e8733df1c716566.png)
新的结论具体怎样,让我们拭目以待。
One More Thing
陶哲轩可谓是AI工具的忠实粉丝,Copilot、GPT-4,还有一些其他辅助工具都受到过他的推荐。
这次,他还对大模型的发展提出了新的期待,希望有一天模型可以直接生成不等式变体。
![陶哲轩疯狂安利Copilot:它帮我完成了一页纸证明,甚至能猜出我后面的过程](/wp-content/uploads/replace/89545ec317d93f60413c724f4ea8ba9b.jpeg)
论文地址:
https://arxiv.org/abs/2310.05328
参考链接:
https://mathstodon.xyz/@tao/111271244206606941
- 几何朗兰兹猜想被解决!历时30年、证明论文达800余页,中国学者陈麟系主要作者2024-07-23
- 开源大模型杀疯了!Mistral新模型三分之一参数卷爆Llama 3.1,“新趋势已显而易见”2024-07-25
- GPT-4o mini登顶大模型竞技场,奥特曼:两个月内微调免费2024-07-24
- 英特尔CPU疯狂崩溃,测评大佬揭露工艺缺陷,官方回应:修复补丁下月上线2024-07-23