作者Bugquan (靠近边缘)
看板Math
标题Re: [其他] 确定性的失落？创造性的无限？(上)
时间Thu Nov 6 11:24:36 2025
※ 引述 《ginstein (迈向学术之路)》 之铭言：
:
: 本文为前沿数学探索，是数普文非学术文、非公认理论，
:
: 盼能促进 AI 数学家早日到来。
:
现在当然有的数学家引入AI
像是Terence Tao自己就玩的不亦乐乎，还有Timothy Gowers也是
偶尔会分享自己用AI 搞定了什麽
但是最大的问题是，你看这俩菲尔兹奖得主，AI的证明有没有了唬烂或是跳步之类的
他们两个稍微排查很快就能得出结果了
但是对於其他人门槛不够的，最多只能当为辅助工具来用
主要步骤还是得靠自己，不然有时候被AI骗了都不知道
--
※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 106.64.112.48 (台湾)
※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1762399478.A.967.html
1F：→ mantour : AI不断快速尝试各种思路，然後可以自己初步排除掉 11/06 14:27
2F：→ mantour : 一些明显错误的，剩下的candidate再给数学家去检查 11/06 14:27
3F：→ mantour : 。问题是AI提供的解答中黄金：垃圾的比率是否足够 11/06 14:27
4F：→ mantour : 高，如果垃圾比率太高也是形同浪费数学家检查的时 11/06 14:27
5F：→ mantour : 间。 11/06 14:27
6F：推 LPH66 : 话说回来, 我看到有一篇论文是他们用 ChatGPT 产生 11/06 20:35
7F：→ LPH66 : 了 Lean 程式码并且成功编过了, 这种应该算是生成式 11/06 20:36
8F：→ LPH66 : AI 的一种意外应用方式吧 (Lean 程式码能编过表示 11/06 20:36
9F：→ LPH66 : 逻辑推理是通的) 11/06 20:36
10F：→ LPH66 : 这是那篇论文, 做的是 Erdos 曾经悬赏一千元的猜想 11/06 20:38
12F：推 mantour : 谢谢L大分享的论文 11/06 22:13
13F：推 pmove : LLM靠的还是机率吧，能编过不代表逻辑是通的（回L大 11/07 06:54
14F：→ pmove : ），至於机率是否能产生逻辑，见人见智，但有些人认 11/07 06:54
15F：→ pmove : 为无法，所以AI可能还需要基本架构的革新 11/07 06:54
16F：→ pmove : 编译过，只代表compile 会过，不代表执行结果正确或 11/07 07:44
17F：→ pmove : 逻辑通 11/07 07:44
18F：推 LPH66 : 那是其他程式语言, 但这篇论文用的是专门用於证明的 11/07 08:50
19F：→ LPH66 : Lean, 就我所知 Lean 程式编过就表示逻辑推论是通的 11/07 08:50
20F：→ LPH66 : 这篇论文的作者有说他们在这之前不会 Lean 11/07 08:52
21F：→ LPH66 : 但经 ChatGPT 的辅助他们能够将整篇论文的多数结果 11/07 08:54
22F：→ LPH66 : (特别是主要定理) 全部都用 Lean 验证过 11/07 08:54
23F：推 pmove : 回楼上，受教了，谢谢。 11/07 13:48
25F：→ mantour : LLM很擅长翻译，把论文的定理转化成Lean再去检查推 11/11 07:14
26F：→ mantour : 论是否通过应该办得到，不过如果使用的数学家本身 11/11 07:14
27F：→ mantour : 也不是很熟悉Lean，有没有可能在LLM辅助下写出的Le 11/11 07:14
28F：→ mantour : an跟本来要证的定理其实是不等价的 11/11 07:14
29F：推 LPH66 : 原论文也有讨论到这个问题, 但恰巧他们这个问题 11/12 22:58
30F：→ LPH66 : 比较着名 (Erdos 悬赏过的问题) 有其他人已经做好了 11/12 22:59
31F：→ LPH66 : 这种「翻译」 11/12 22:59
32F：推 ginstein : 创作不易，感谢回文评论！ 11/18 09:12