关于AI主题的草稿

• ai is not new.
• post ai math and mathematicians
• post ai

新事物会带来变化；但是『事物变化」这件事却是相当古老的。

工业革命。

效率越高，资源越紧缺的悖论。

人类早就变了。

曾经被看作大逆不道或者违反人类本性的变化，早就被接受了。

新新人类是创造人类的人。他们没有旧包袱。

但这些都是大图景下的看法，在当下时代的具体的人身上。 纺织工和程序员是真正在被淘汰的。

最近（2026-05-23）关注了一下用AI做数学研究的近况。翻了下arxiv发现之前的合作者在一个月内用AI狠狠写了五六篇论文挂上去。

不得不说真的慌了，这还做个P的研究啊，本来就垃圾，现在更没用了。刚出现AI绘画之后，本以为数学是最后被干掉的学科，现在发现这个认知也许是错的。 或者说，（以人类方式理解的）数学很难被干掉，但古典数学家很可能被干掉。

数学家的功能？

很多工作/职位/身份是随着技术或其他东西变化而变化的。 比如曾经没有专职程序员，而是由科学家、计算机学家等编写代码，这是他们工作的一部分。 曾经也没有数学家，只有科学家，或者只有哲学家或智者。 曾经也没有产品经理。有人想做某个东西，然后就做某个东西，而不是告诉别人要做什么东西，然后让别人实现。

以后数学家的角色，后者说其后继的角色，是审查（AI生成的）数学并加工。

同样在程序员领域，很多人的担忧是，现在能出色使用AI的人本身就是高等级的程序员。像Linus很早就不写代码而用能工智人了。 但是随着AI进入越来越fresh的程序员工具箱，我们还能有新的高级程序员吗？

类似的现象是不是也出现过？被替代后的工作/技艺的失传。在AI之后会发生什么呢？

vibe math

barlec

vibe coding: 人提供方向和意图，AI负责实现细节。

编程：有编译器、测试反馈。 数学：证明正确性难以自动验证。 但形式化验证 = 数学编译器，使 vibe math 成为可能

aletheia DeepMind. 1stproof.org

形式化的重要性 数学论文错误率不低。 Voevodsky 的论文有错误。 四色定理，Kepler猜想，Feit-Thompson定理

lean 使用 mathlib

Math Inc E_8 球填充问题

Lean的可靠性是否可能被哥德尔不完备定理限制？

Phrase 1 formal 搜索树的证明思路 HyperTree AlphaProof IMO 金牌 Phrase2 Informal + Formal (2023-2025) Draft, Sketch, Prove DeepSeek-Prover-V2 Kimina Prover Phrase3 agent Archon 三角色, Gauss(Math Inc) 多工作流编排, Aletheia (DeepMind) 自主研究 Plan Agent, Informal Agent, Lean Agent. tools: Mathlib, LSP, REPL

AI4Math 怎么创业？ Axiom Math

2026 Moonshine 产生新猜想 Neural Jacobian Conjecture LeanConjecturer Funsearch AlphaEvolve

Tao 积极使用AI AI will not replace mathematicians, but mathematicians who use AI wull replace those who don’t.

数学会像程序员一样，以后变成工科吗？

AI能提出问题吗？能提出好问题吗？AI的taste和人类的taste？

AI能搞出新工具、方向吗？

高质量标注来提升AI的数学品味？

数学问题的起点的占比（初始预料/提示词占比）？AI的“完全”原创成果可能吗？

人类在AI4Math的功能：承担责任，署名论文要为结果负责。 （艺术、文学，没有对错，如何背锅呢？） gpt能写在作者栏吗？

数学本身还很安全

持一种柏拉图主义的态度。并不是说数学柏拉图主义是对的，而是说我的态度、行为基础、视角倾向于此。

做数学的人要完蛋了

或者说，做数学这件事的含义要改变了。 进而，在人类世界显现的数学先要改变。

后AI时代的数学工作者

https://leidendeclaration.ai/

审论文怎么办，就像代码 review

程序员世界发生的事，很可能在数学界再发生一次。 比如铺天盖地的pull request，重复的论文

在 AI 绘画出现、程序员开始紧张时，我持有的观点是，数学可能是最后被 AI 冲击的行业，甚至到两三个月之前也这么认为。但某种意义上，现在我并非放弃最初的看法，而是对它做更详细的描述，尤其是补充外围。

要澄清多个概念： AI 能做的事，能代替人类做的事，有什么 AI 做的能取代人做的，以及这个事/成果本身。

在部分人群中似乎有一种观点，认为当 AI （具身的）能做到所有人能做到的事，人会陷入到一种无聊，考虑到也许艺术这类事也会被取代，人会无所事事。 这大概是某种技术奇点主义/赛博弥赛亚情节的负面想象下的想象。 这种想法的问题在于，技术奇点或赛博弥赛亚本身是可疑的。生产力发展和生产力解放、生产关系解放，并不是一回事。也许 AI 最终能做所有事，但并不会取代人去做所有事。 现在已经出现 Token 比程序员更贵的倾向了。

更简单的例子是，当社会财富暴涨时，出现的情景往往是夫人更富，而非财富公平。 放眼于这个神话的“无聊”负面影响的人，往往是那先现在就无聊的人，或者说 be capable to feel bored 的人，不用担心工作消失的人，他们会在工作真的消失的时候感到无聊。另一种可能，是那些相信技术奇点的人，会认为人会面临无聊。

在双清的报告里，最后 菲尔兹奖得主 Caucher Birkar 做了个小结。看起来 AI 做数学超过人是迟早的事，但我们人类依然会继续做数学。 远在 AI 出现之前，像深蓝这样的计算机（算力怕是比不上小天才电话手表）就能在象棋上超过人类。但是现在每个城市、每个大学（可能是他经历里的大学吧），都仍然有棋类俱乐部、棋类比赛。 数学家做数学，其实不是为了那个数学成果本身，而是在研究中体验到的智识上的享受。¹

一方面，即使 AI 能做所有事，也不会代替人做所有事。另一方面， AI 做的事并不能代替人做的事。并非从成果本身而言，而是从制造过程而言。当下机器速冻水饺流程已经充分成熟，但手工水饺依然有一席之地。²超加工食品盛行之下，全天然纯手工食品又有另外的价值。 以后像手工绘画、手工代码、手工数学证明等也许也会成为这种商品。

但这些不是我反驳 “AI冲击数学” 的角度。因为受到冲击的事数学家（的职位），并不是数学本身。 从数学的柏拉图主义来看，数学是一个柏拉图意义下的实体，并不存在于现实，也与现实无关；而数学家仅仅是窥探数学世界，是一种探索和冒险。 数学是一个以公理和定义为基础、以纯粹逻辑³为手段来构造的。在这个意义下，数学和计算机领域是十分类似的。当然也可以十分激进地说，计算机领域完全可以视作数学的一个分支，详情见图灵机、lambda演算、可计算性理论等。至于实际写代码、做工程，基本上可以是做应用数学。

现代集合论奠基人康托尔称，数学的本质在于它的自由。数学和计算机有不同的自由也有各自的限制。数学的限制更多在于人的选择，比如（大部分）人选择了选择公理的数学世界。而计算机的限制则来自某些物理现实的基础，毕竟要在CPU上跑程序。 二者其实都因为人的偏好而偏向某个范围。比如 $\mathbb{Q}$ 上的常见的范数和$p$-adic 范数，人们更熟悉前者，而后者却了解不多。在计算机领域，x86指令集依然占统治地位，而 ARM 似乎有发展趋势，除此之外还有 loong 架构这种“无人问津”的小众宝藏指令集。

二者的一个相似性在于，其底层本身是简单的，却在复杂问题下快速变得极度复杂，人类（在实践上）无法读写。真正读写的内容往往是多个中间层之后的高度抽象语言。 例如机器上可执行二进制程序读取的是机器码，机器码之后是汇编，然后是C语言等高级语言。 在数学领域，比如说线性空间的张量积，这在前沿数学里是一个非常基础的概念，但离最底层的定义有很多抽象层。张量积的定义依赖多重线性映射的泛性质，这建立在线性空间和线性映射到基础上；线性空间是域上的模，这里又需要群环域模的定义。 甚至实数域 $\mathbb{R}$ 的定义也不简单，要从皮亚诺公理开始，一路经过数学归纳法定义正整数集、定义加法、乘法，证明结合律交换律，把幺半群 $\mathbb{N}$ 扩充到整数环 $\mathbb{Z}$，通过局部化得到有理数域 $\mathbb{Q}$，最后再加上完备化达到$\mathbb{R}$⁴。 线性空间的直和、张量积之于代数学家，就像整数加减法之于普通人一样，是熟悉、显然的构造。

综上，事实上用计算机做数学是非常容易的。问题在于，做出怎样的数学？怎么避免正确的废话？

人类在数学上有一个悖论式的处境：人类没有理由能理解数学，因为数学没有可供理解的意义；但人类严重依赖于对数学的理解来研究数学。 在我眼中，这是数学之于人的神秘魅力。

但这也意味着， AI 做数学同样不需要理解数学。只需要它大量产生正确的废话，从中自然会涌现出可被审美的结果。

数学家被冲击了，但数学本身安然无恙。甚至我们其实根本不知道，数学的恙是什么⁵。