AI 时代：代码、数学、相机与未来

聊代码和数学前，先聊一下数码相机，这样才不至于被自己的职业局限，无法打开想象力

胶片时代，一卷胶卷就那么几十张。每按一次快门都得想清楚：光够不够，构图对不对，值不值得用掉这一张。拍完还要等冲洗出来，才知道哪张能用。

1975 年，柯达工程师 Steven Sasson 做出了第一台手持式数码相机。它重 3.6 公斤，只有 100×100 像素，存一张黑白照片要 23 秒，画质远远比不上胶片。

截至今日, 我们对数码相机习以为常, 但站在历史的角度, 他改变了一件非常要紧的事：按快门的成本。

拍完马上能看，不行就删掉重拍。胶卷、冲洗这些琐碎慢慢退场，摄影师的心思可以更多地放在「拍什么」上。

后来的事，大家都知道了。2023 年发布的 Sony A9 III，1 秒能连拍 120 张，电子快门最快到 1/80,000 秒，快到能把溅起的水花冻住。

图中水花照片：A. M. Worthington，《A Study of Splashes》，1908，公有领域。

为什么聊代码和数学要先聊这个？因为作为工程师，我很长一段时间都活在古法手作「胶片时代」。

在工作中我经常需要验证各种实现思路, 作为人类, 我经常意识到自己的渺小。几个方向摆在面前，听起来都说得通，可我的精力蓝条只够认真验证一个。剩下的，就进了「以后有空试试」的清单。

AI时代来了后, 一切发生了变化. 我养成了一些「奢侈」的坏毛病, 比如 PR 里会有大量的提交, 开很多 worktree 实现我的思路, 最后选一个最好的版本, 这在以前古法时代是难以想象的.

AI 其实就是工程师的数码相机

AI 就是我代码的数码相机

最近我在用 Claude Opus 5.5 和 GPT-6 Astra 写视频编辑器、调 Metal，做一个原生的视频编辑器，经常要在几种语言之间来回混编。

放在以前，光是跨语言就很耗蓝。每换一种语言，就要换一套工具链、一套调试方法，脑子也得跟着切换。GPU 上的问题更磨人：画面错了，往往不报错，只是「看起来不太对」。优化也非常难做, 但 AI 这个源神就不一样, 我觉得有一个地方可能 CPU 性能不好, 加了一些 hack 的做法, AI三下五除二先编译二进制, 然后反编译看汇编告诉我你这个优化没有意义.

现在，样板代码、跨语言的衔接、各种检查工具，这些琐碎的活我会先交给 AI。

视频编辑器里有很多细致的算法。以前验证一个要花不少时间，很多时候只能凭肉眼看看，差不多就算了。现在我会先让 AI 写个检查工具：抽帧、逐像素对比、把差异画出来。以前舍不得按的快门，现在每改一次都能按一遍。

省下来的精力，我留给了想象力。方向没定的时候，多想几种架构，让 AI 把几条路各搭一个最小原型，跑一跑再说。

写到这里，我想明白了一件事：AI 其实就是我代码的数码相机。

它没给我无限的蓝，只是让每次施法便宜了。

当然也要清醒：测试通过，只说明测到的情况没问题。没测到的，还得我自己想。

答案很简单，找到它很难

写代码越久，我越有一个体会：最后留下来的答案，往往没那么复杂。

很多 bug 查了好几天，最后只改一两行。难的是找到那一行。

有个很有名的例子。Jon Bentley 在《编程珠玑》里写过一版二分查找，证明过，也测试过。大约二十年后，Joshua Bloch 指出它有 bug：数组很大时，(low + high) / 2 会整数溢出。修法只要一行。

说实话，我自己也写过 (low + high) / 2。

数学里也一样。2012 年底，黄皓第一次听说敏感度猜想，把它放进了自己的「秘密清单」，每发完一篇论文就回来试一阵子。2019 年，他终于证明了它，前后七年左右，核心证明只有两页。

开头我说，我也有一份「以后有空试试」的清单。区别是，他一次又一次回去了。

Hoare 在图灵奖演讲里说过：构造软件设计有两种方法，一种是让它简单到明显没有缺陷，另一种是让它复杂到没有明显的缺陷。第一种要难得多。

一张好照片看起来很简单，印样上却可能是几十格废片。多按几次快门，是为了找到那一张简单的；但判断「就是这张」的，还是人。

数学界的 Bug Bounty

超衍智能（Apex Intelligence）设立了一个10万元的学术公开悬赏，分三个奖项：重大漏洞奖、关键验证奖、突破贡献奖。

我的第一反应是：这不就是给数学证明开的 Bounty 吗？

第二反应是：可惜我是工程师，不是数学家。

超衍智能的创始人是清华人工智能学院助理教授陈勇超，合作团队包含清华等高校的数学家。据活动方介绍，他们的 AI 系统与合作研究者完成了 5 项数学研究：2 项已完成专家核验，3 份是候选论证，正在公开征集独立验证。

这些前沿证明我判断不了，但有个细节我很熟悉。

在 Halpern 迭代相关的论文里，团队披露了 AI 的使用方式：先借助 AI 找到一版结果；研究者核验之后，提出更强的目标；再借助 AI 继续寻找证明；研究者再核验。

这个节奏我太熟了：先有个思路, 让 AI 狂烧 token 跑通, 最后给自己的工作打分，我来 review，提更高的要求，再跑一轮。据介绍，这套方法作为原创的 AI for Math 方法论级案例，一个月内先后被清华、北大和 Google Research 跟进引用。

三个奖项，也能对上软件工程里的老朋友：

• 重大漏洞奖：找出证明缺口或反例，像红队和 Bug Bounty。

• 关键验证奖：独立核验、形式化验证，像 Proof Of Concept。

• 突破贡献奖：修复缺口、显著简化证明，像修复和重构。

数学史上早有这样的「提交记录」。假设我们把四色定理的 147 年写成了一份 git log, 那么他就是这样的.

图中插图：Kempe 1879 年论文原刊 Plate II（American Journal of Mathematics 第 2 卷）；Kempe、Heawood 肖像来自 Wikimedia Commons。均为公有领域。

Kempe 的证明被接受了 11 年，才被 Heawood 找到漏洞。这段历史里没有 AI，但一个定理从提出到站稳，三种贡献一样都没少。

试想一下，有了 AI，数学家是不是也能省下更多的蓝，多探索几条路，为世界带来更多有价值的发现？

未来：AI 会走进更多地方

代码是较早用上这台「数码相机」的地方。接下来，AI 会走进更多领域。

我很期待这样的画面：数学家或各领域的专家，随手一个想法，就可能和 AI 碰撞出不一样的火花。以前因为没蓝而放下的那条路，也许能先试一试。

但火花多了，验证就更重要。就像照片多了以后，值钱的变成了两件事：会选片，以及经得起放大到 100% 的那几张。

我觉得，「超级个体」也可以是这样的：一个专业研究者，带着 AI，多探索几条路，把其中有价值的部分做扎实。

超衍智能对这次悬赏的态度，我挺认同：对尚待独立验证的内容不预设结论；能否成为可靠成果，要看每一步经不经得起复现、质疑与验证；发现实质问题，对应的论证和状态也会更新。

在我看来，这就是把验证这一步公开出去，像开源项目欢迎全世界来提 issue。

相信在未来, 更多的领域会密集使用到 AI, 世界也会因为 AI 进步飞快.

邀请与收尾

这次悬赏总额 10 万元人民币，奖励经评审核实的贡献。公开征集独立验证的，是那 3 份候选论证：凸形 Nivat 猜想（悬而未决 29 年）、Souto 猜想亏格二情形、Kakimizu 复形可缩性。

不必一上来就挑战整份证明。就像参与开源，很多人是从一个 good first issue 开始的：认领一条关键引理、一段归约，或者一个估计。

提交时要写清四件事：对应的论文版本、命题位置、具体理由、可复核的推导或代码。在程序员眼里，这就是一份合格的 bug report。

面向数学及相关学科的高校研究者、独立研究者、擅长 AI 工具与形式化证明的开发者；也欢迎数学与科技内容创作者组织公开讨论。

也说一句分寸：多问几次 AI，不等于完成证明；计算检查，也代替不了一般性的数学论证。AI 提出的质疑，同样需要核实。

数码相机没让我变成摄影师，但它让我敢多按几次快门。如果你本来就是「摄影师」，这台相机也许能帮你多试几条路，再把值得精修的那几张做扎实。

把省下来的蓝，留给想象力。

提交入口：math.apexin.net

奖金分配、评审安排和活动时间，以活动详情页为准。