*讨论记录：数学与做数学
因为基础数学拔尖交流会听了一天的讲座。中午时与两个同学（以下记作“水母”、“烧杯”）逛湖、讨论分方向要去什么方向之类的重要问题，这里略作整理（不过只能保证大意）。
I
上午姜杰东的《数学形式化与自动形式化》讲座提及，AI 对单篇论文进行的形式化往往不具有可复用性，因此有一个愿景是有更大版本的 mathlib，将整个数学形式化，之后每有一个论文大约花费 100 元1就可以得到一个形式化版本。
【水母】……然而我们想要验证一个定理陈述的形式化是比较困难的，因为没有对形式化语言的直观。
【我】我感觉，知晓对应概念的人最多花一个月就能验证对应的陈述是否正确……？
……
【水母】开源社区中成员之间互相检查不能保证内容的正确性。
……
【我】实际上我们对于 AI 还有一种愿景：它能够联系现实，从而直接知道我们应该去建立什么框架。在此种意义下就真正地完全不需要人类了。
……
【我】我认为我没有从你那里听到什么新的东西，实际上那个主讲人也没有给出任何新的东西。数学的此种发展前景是显然的。
【我】实际上更早的时候就可以发现这一点。如 Trebor 的回答：
一阶逻辑已经被完全解决了啊。高阶的逻辑，要么已经证明不可能是 decidable 的，要么也都解决了。
就算是 undecidable 的问题，也有类似 Coq 的 tactics 系统，可以有效的给出定理的证明。我觉得一个（强化学习的）神经网络加上蒙特卡洛方法，就可以像 AlphaZero 一样指导自动证明了。
事实上，数学证明与编程语言非常相近，简直就是一样的（Curry-Howard 同构），所以计算机处理数学证明非常方便。
【我】邪恶地说，我不关心数学的前景如何。我关心我能从中得到什么。或者说，在这样一个背景下我（如果还学数学）应该如何赚钱。
【烧杯】可以去做这一块的 AI。
【我】但是这是一次性的。有了之后，就不再需要人了。
【烧杯】可以去做形式化仓库的维护员。
【我】那他们每个月给我多少钱呢？感觉不会有多少。
【水母】可以做教培。
【我】我认为像教培这样的东西会很快消失。
【水母】我反而认为教师这种职业会永远存在。
【我】但是，至少对于数学，人来教有什么比 AI 更好的地方呢？比如我现在感受是听课远没有看课程讲义有用。
【水母】人可以带来情绪价值。有一种与人的连接。你觉得他们为什么要去找家教呢？
【我】因为他们觉得向来如此……没有意识到（这个时代）完全可以自学。
【水母】像现在很多大学生家教，实际上不一定比真的教师教得好，但是他们看中这个牌子。
【我】我认为这是不能长久的……这样的事情应该越来越能够被澄清，大家会逐渐意识到这一点……
【水母】不一定如此。
……
【我】那就相当于是，“赚傻子的钱”？
……
II
【水母】我们应该讨论一些具体的东西。
【我】现在有一些新成立的 AI for math 公司……比如董彬的创业、子鱼的 UltraFilter……应该看看他们是如何商业化的。
【烧杯】所以问题是他们为什么会得到投资。或者说，为什么投资者相信能够得到回报？也许是认为有可能有用，计算期望后可以给出对应的投资。
【水母】我们应该想一下学校为什么要给数院经费。…………
【烧杯】应该想一下，人们为什么会觉得学数学有前途呢？
【水母】
- 基础数学有的时候真的会有实际应用；
- 可以顺手培养输出数学人才；
- 基础数学研究被社会认可，如果做得好可以吸引资源。
【我】第 2 点貌似是为了第 1 点……或者是提升工业界数学水平。
【烧杯】为什么会被社会认可呢？
【水母】可能是一个制度体系的结果（某种大学和期刊主导的学术界的秩序）。
【我】如果没有很好的别的原因的话。我担心这样的价值会被消耗……实际上正在被消耗。
……
【水母】人们觉得学数学的比较聪明……？
……
【烧杯】……这是一种社会意识。
……
【水母】数学开始脱离实际，其实是很晚近的事情……？
【我】我觉得至少一直到弦论，人们至少主观上是希望用于实际的。而今天看，似乎我们天然觉得数学是可以完全脱离实际的（注：现在想想存在应用部分被分离出“基础数学”的原因）。这中间有一个 gap。
【水母】那为什么会这样呢？
【我】我想想……回忆 Hölder 那个纲领……实际上我现在也不知道有限群有什么用（注：现在想想能少许用于密码学），Lie 群则对物理有用。然后有很多人去做那个大项目……
【烧杯】应该是有一些具体的现实因素。只是因为一个人想错了不会导致整体都这样。
【我】嗯……我还有个想法是因为具体的问题都太复杂了，而数学又要发展……故只能往抽象的方向上走。
【烧杯】所以说，可能很多数学家找错了命题（考虑的其实是不重要的命题）。
……
【我】（回忆周三听的邓煜关于 Hilbert 第六问题讲座）邓煜的证明中能用 collision history diagram 是因为做了硬球的设定……对于实际（Lennard-Jones 势等）的情况可能完全没有用。
III
【烧杯】所以对一个定理给出证明有什么价值？
【水母】通过证明一个定理可以找到工具、建立理论…
【我】所以人们寻求的是更高的看问题观点，直到没有更高的观点。
【烧杯】但应该是社会存在决定社会意识……
【水母】为定理给出证明可以为提出新的定理陈述、建立新的理论体系打基础。
【烧杯】定理可能会带来确定性。
【水母】似乎很多时候经验上正确但没有被证明的东西也可以直接拿来用。
【我】所以按照我之前的想法，证一堆 with probability 1-δ 某某界似乎是大有可为的……不过感觉 AI 会适合证这种。
【烧杯】确定性可以使得，我们用它来做机器，可以避免潜在的财产损失。
【烧杯】所以如果 AI 证明定理的能力很强，人类数学家会失去通过证明定理创造价值的途径。那么人类其实寻求的不是证明定理本身。
【我】我重新陈述一下前面（水母）的想法：通过证明定理人们可以看到其条件可以推广到何种地步……那人们寻求的是这一点而不是证明定理本身。
【水母】人类数学家需要通过理解和整理定理的证明，提出新的定理和理论体系。
……
【水母】似乎很多时候经验上正确但没有被证明的东西也可以直接拿来用。
【我】就我现在对机器学习中定理的所知……它们可以用来指导改进的方向，知道有些方向为什么永远改不好……但往往是先有某个方法然后再建立对它的解释。
……
【烧杯】最重要的是 AI 的证明能力能到什么程度。我们要讨论的是现在的情形还是未来的情形。
【我】我认为到 2028 年差不多可以做到给一个定理可以在一小时内证明。
【烧杯】在定理证明这一点上我们是与 AI 相对立的。
【烧杯】我刚刚说的不对，AI 应该视作工具。
【我】但是与使用 AI 的人是相对立的。
……
【水母】我们应该回到做数学有钱拿的时代，看那个时候是因为什么。
【我】（回忆笛卡尔）以前是贵族养着数学家算炮弹轨迹。然后空的时间可以做一点研究。
……
【水母】我认为重要的是新的定义。
……
【我】我认为 AI（即使是现在版本）也有提出新理论体系的能力（只不过尚未显现）。
……
IV
【烧杯】我们应该停止 DFS，而是 BFS，回到开始的问题……
……
【烧杯】一个数学家能做什么？我们要先讨论数学家的定义……
【我】实际上应该讨论的是，有数学能力并且有对应的凭证的人，能做什么。
……
下午李智强的讲座的 PPT 引用了 Stefan Banach 的经典名言：
A mathematician is a person who can find analogies between theorems; a better mathematician is one who can see analogies between proofs and the best mathematician can notice analogies between theories. One can imagine that the ultimate mathematician is one who can see analogies between analogies.
讲座中提到 Sullivan 的字典复活了复动力系统。字典是一种可以生成 conjecture 的 meta-conjecture，于是说“如果想要最少地变化（继续学数学）……在 AI 背景下原本的 mathematician 应该 be a better mathematician；better mathematician 应该 be best mathematician……”另外提及认为基础数学动力来源有三个：数论、几何、物理。
【交流会结束语】在这样一个动荡的时代……
在这样一个动荡的时代。
【水母】其实有一点我中午没说，就是人类数学家还需要把控数学的品位。问题是无穷无尽的，我们需要选择发展的方向。我觉得，问题的应用价值可能会在这种选择中占更大的分量——数学将要回归实际。
【我】你回到 Part I 了。
之前 Poincaré 猜想的形式化大约花费 15000 美元。