logo
Redian新闻
>公众号
>
陶哲轩：我用GPT-4辅助证明不等式定理，论文还会上传arXiv

陶哲轩：我用GPT-4辅助证明不等式定理，论文还会上传arXiv

公众号新闻

机器之心报道

编辑：杜伟

陶哲轩可太喜欢 GPT 系列大语言模型了！


近几个月来，著名数学家陶哲轩热衷于用 ChatGPT、GPT-4 等 AI 工具辅助解决数学问题。我们也一直在持续地关注，这不今天又看到了他使用 GPT-4 来帮助自己证明数学定理。

不禁好奇，是什么样的数学定理呢？

根据陶哲轩的介绍，他最近在包含有限多个实变量的不等式理论中有一个完成的示例结果，并很快会发表在 arXiv 上。

因此，他最终决定开始了解 Lean4 交互式证明系统，使用必要的辅助 AI 工具（GPT-4）来帮助自己来使用。他希望能够实现相当简单的形式化。

我们也搜到了一篇陶哲轩的关于麦克劳林（Maclaurin）型不等式的论文，不知道是不是同一篇。


论文地址：https://browse.arxiv.org/pdf/2310.05328.pdf

陶哲轩在 IPAM 机器辅助证明研讨会上看过几次 Lean 演示，在那里有人建议他玩一玩自然数游戏，以此熟悉 Lean 中用来证明定理的基本语法和策略。

他发现自己很能上手这个游戏，其中证明结果与其本科实分析书中前面的章节非常相似，比如根据皮亚诺公理建立乘法交换律和结合律等基本算数事实。此外还让他想起了自己在《QED-an interactive textbook》中编码过的逻辑游戏。

大约 3 个小时后，陶哲轩玩到了「高级乘法」，并计划之后在空闲时间继续玩下去。


自然数游戏地址：https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game

然而，考虑到自然数游戏中有限的可用工具集，陶哲轩还没有发现 GPT-4 对解答该游戏直接有用，它给出的解答方案通常包含未纳入游戏的方法。不过，他发现 GPT-4 当然对 Lean 很有帮助，他可以从中得到有关问题的有用答复。

随着关卡越来越难，GPT-4 肯定会更有用。比如，在 Z 是 X 的明显结果以及 Y 正在解决各种微妙语法问题（否则这些问题会非常令人沮丧）的情况下，问它「如果我知道了 X 和 Y，如何证明 Z 呢？」。陶哲轩发现，自然数游戏似乎拥有比文档实际披露的更多的 lean 库。

对于陶哲轩的尝试，有网友表示很酷。Lean 非常好。有很多工作需要编写经过验证的证明检查器，比如 SAT、SMT、sharp-SAT 等也使用 Lean。


还有人问陶哲轩，「如果让你猜的话，LLM 需要多少年才能拥有超越全人类的写证明能力呢？」



看来，要想回答这个问题，陶哲轩的大模型试验之旅还将继续下去。

博客链接：
https://mathstodon.xyz/@tao/111206761117553482



© THE END 

转载请联系本公众号获得授权

投稿或寻求报道：[email protected]

微信扫码关注该文公众号作者

戳这里提交新闻线索和高质量文章给我们。
来源: qq
点击查看作者最近其他文章
相关阅读
陶哲轩：用 ChatGPT 写代码太省时间了GPT-4成功得出P≠NP，陶哲轩预言成真！97轮「苏格拉底式推理」对话破解世界数学难题陶哲轩发新论文了，又是AI帮忙的那种北去恋江南，南归思亲情——我的上海老乡微软开源的大模型太强了，数学推理超ChatGPT，论文、模型权重全部公开陶哲轩上手Copilot：不可思议，它能从定理名字猜出我想要的方向陶哲轩疯狂安利Copilot：它帮我完成了一页纸证明，甚至能猜出我后面的过程红色日记 8.1-10陶哲轩又来安利AI工具了：新论文排版用上VSCode Copilot+插件陶哲轩新论文：部分证明著名素数猜想，新方法用到了自己的旧模型像搭乐高一样做数学定理证明题，GPT-3.5证明成功率达新SOTA真香！陶哲轩：用ChatGPT写代码太省时间了！GPT-4野生代言人陶哲轩：搞论文学新工具没它得崩溃！11页“超简短”新作已上线莫须有罪名与疑罪从有Erklärung zur Zusammenarbeit中美双重税务居民身份持有人的3个不等式获1000万美元捐款，用于代码重构、上云，论文预印版平台arXiv「好起来了」GitHub Copilot让陶哲轩感到“不安”陶哲轩支持！AI奥林匹克数学奖来了，奖金500万美元，寻找能得IMO金牌的大模型陶哲轩：初学者不宜用AI工具做专家级任务，GPT对专家帮助不大陶哲轩再逼近60年几何学难题！周期性密铺问题又获新突破魅族新机预热 祭出边框不等式；华为天气上线App免广告权益；阿里云大面积瘫痪MiniGPT-4升级到MiniGPT-v2了，不用GPT-4照样完成多模态任务陶哲轩论文漏洞竟被AI发现，26年预言要成真！看定理名猜出研究方向，大神直呼AI能力惊人ChatGPT Plus推出邀请制！可以让朋友免费用GPT-4了，最长90天陶哲轩用大模型辅助解决数学问题：生成代码、编辑LaTeX公式都很好用AI颠覆数学研究！陶哲轩借AI破解数学猜想，形式化成功惊呆数学圈《花尾渡》（小说） 第十八章 一半的天堂凉凉!开学了，论文进度0，某研三医学生在组会上被公开处刑，结果......中国科研论文蝉联“三冠王”，论文数量、质量及引用次数全面领先我用GPT，找了40918份远程工作陶哲轩：GPT-4神助攻，写Python代码轻松省半小时5134 血壮山河之武汉会战 信罗战役 7刚刚开源！中科大提出利用GPT4-V构建大规模高质量图文数据集ShareGPT4V，助力模型霸榜多项多模态榜单！「陶哲轩×GPT-4」合写数学论文！数学大佬齐惊呼，LLM推理神助证明不等式定理
logo
联系我们隐私协议©2024 redian.news
Redian新闻
Redian.news刊载任何文章，不代表同意其说法或描述，仅为提供更多信息，也不构成任何建议。文章信息的合法性及真实性由其作者负责，与Redian.news及其运营公司无关。欢迎投稿，如发现稿件侵权，或作者不愿在本网发表文章，请版权拥有者通知本网处理。