从现在开始不要学数学了，学数学就是浪费时间

这就好像你按计算器可以解决的问题 你也得知道怎么按啊 相当我们需要了解的数学基础可能从中学二年级降到了小学三年期的程度 是一个大的变化

Push-forward 发表于 2024-7-26 13:22
又来低级喷了。每次忘了在贴自立加这么一句总有低级喷。
我在北美top30 数学phd program，之前做的是str ...

哥们很好奇你学了这么多年数学phd 是怎么把imo的初等数学问题和高等数学的research联系起来的

Push-forward 发表于 2024-7-26 13:22
又来低级喷了。每次忘了在贴自立加这么一句总有低级喷。
我在北美top30 数学phd program，之前做的是str ...

而且说实话 我感觉大模型更新定理 改进上下界没问题 但是提出真正有意义的conjecture which is the key in math 大模型不一定能做得出来 我觉得这很显然是一个很强大的辅助工具 以后的数学界大概是少数掌握方向的大师 加上一部分负责微调的牛人 以及辅助ai 像那种专门解决toy case的数学家可能要丢掉饭碗了 最后我觉得兄弟 就算你转行了 没必要对纯数这么嗤之以鼻 这种本质上的润人心态不该是一个曾经fully dedicated into math的研究者有的心态

小虎虎123 发表于 2024-7-26 17:55
哥们很好奇你学了这么多年数学phd 是怎么把imo的初等数学问题和高等数学的research联系起来的

这个工作不一定意味着LLM可以做research math，但意味着经济活动中的绝大多数的数学推理工作完全可以由LLM替代（比如software verification，精算等等）。

除了数学家，没人真正对怎么用AI证明黎曼猜想感兴趣。大家感兴趣的是怎么用AI找到更好的交易策略这种事儿。

小虎虎123 发表于 2024-7-26 18:07
而且说实话 我感觉大模型更新定理 改进上下界没问题 但是提出真正有意义的conjecture which is the key i ...

关于找到有意思的conjecture，难点在于设计一套针对“有意思”的metric。这种metric比较elusive，但也不至于完全不知道说不出来，比如这个关于conjecture的metric可以包含：
1. 这个conjecture不是显然的
2. 如果这个conjecture是对的，那么会有很多consequence
3. 这个conjecture符合某种规律，这个规律可以是在别的数学领域中存在的规律。
4. 我们可以轻易的定义一大堆not interesting的metric。
至于能不能最后训练出来，那就得等实验了。

最后，这种润人心态本质是自己吃过苦了，现在出来了，结果发现这个坑马上要变深10倍，希望还在坑里的人赶紧出来的正常人心态。没有AI的时候做数学很苦又穷，有了AI之后大部分做数学的只剩失业一条路了。

现在做数学的人里面大部分人都做不到发现有意思的conjecture。真正具有发现有意思的conjecture的能力的数学工作者是少数，甚至是少数中的少数。至少这大部分人得跑吧？

因为AI能学会并研究一个领域，人类就应该从这个领域撤出来？没这个道理吧？
这是降临派的想法，等着把人类的命运让渡给天网啊。

54188wo 发表于 2024-7-26 18:35
因为AI能学会并研究一个领域，人类就应该从这个领域撤出来？没这个道理吧？
这是降临派的想法，等着把人类 ...

兄弟你会让小孩学翻译吗？

纯外行看神仙打架哈哈，请问lz能简单说说Lean +的原理吗？网上搜一圈，都是说它资源利用率高，不太懂

finnshing 发表于 2024-7-26 18:39
纯外行看神仙打架哈哈，请问lz能简单说说Lean +的原理吗？网上搜一圈，都是说它资源利用率高，不太懂

Lean本质上就是个compiler，可以检查一段证明是不是成功证明了一个定理。你可以绝对相信这个compiler。

Push-forward 发表于 2024-7-26 20:26
这个工作不一定意味着LLM可以做research math，但意味着经济活动中的绝大多数的数学推理工作完全可以由LL ...

我怎么觉得的相反，这个工作恰恰是让AI做证明题而不是建模？

当然研究工作也不仅仅是证明。人类更适合探索发现新的数学现象；判断命题的真假和给出对应的证明的工作就交给AI。各司其职多好。