作为科学的数学

动机

这一篇大概算是讨论科学的系列文章的支线。起因是在一次聚餐听学术八卦时，一位老师提到，他认为现在很多数学论文其实都是错的（要是加上我那垃圾的毕业论文，确实）。

图文无关

全篇图文无关，只是一些好玩的meme而已。

在科学何以可能中就提出，数学并不能算是科学，它不依赖现实世界，因此从本体论和认识论上来说，数学和其他科学（比如物理）是不同的。
方法论上来说也是不同的。科学的方法论是依赖于实验的，而数学的方法论是依赖于逻辑的。

但是两者也有相似之处。应当说，一个理想的与人无关的数学结构，确实是不同于科学的；但人所研究的数学，则与科学有相似属性。

社会建构的数学

福柯认为科学知识是权力的实践形式，也许也包括数学知识。

例如，科学研究的偏向是受现实应用影响的，我们人类会认为这个理论比那个理论更深刻/重要/优美/高端；而数学研究的偏向类似，受其在科学中的应用和实际掌权者的兴趣影响，会倾向于认为这个定理/理论比那个更深刻/高端。
考察一下菲尔兹奖的候选和实际获奖的成果，再看看评选者是哪些人。或者看看高校有哪些方向的人抱团，管理层的人是搞什么方向的。

不可知的错误

另一个相似之处在于知识中的错误。在科学中的错误，即使不考虑人为错误，也可能是不可避免的，很容易持有一种不可知论的观点（类似于人为误差和系统误差）。而数学从形式化的角度看根本没有正确和错误，只有数理逻辑中的布尔值，这个值不是“真”或“假”的含义。纯逻辑而言数学是“可知”的，虽然这个可知范围被哥德尔定理缩小了。
但是一旦在数学研究中考虑人类的因素，似乎人类本身在逻辑上犯的错误，也是一个不可知的因素了。诸如同行审议的方式，是为了论文结论的正确性，但仅仅是一个尝试而已，并不能做出保证。现代数学论文其实充斥着自然语言的论证（因此也充斥着“跳步”），都依赖人类的理解来判断其逻辑正确性，这是十分靠不住的。

没有人了解全貌

而且由于分支的细化，可能某个领域只有少数人理解，如果他们同时搞错了某个步骤，那就完蛋了。同时各个领域互相关联，大部分情况是不加考察地使用不理解的结果（类似于调用外部库）。因此没有人知道费马大定理的全部内容，也没有人完全掌握有限单群分类。

以我自己的论文为例，里面一堆我自己都不懂的东西，我只是把别人论文的结果拿过来用而已。

工程化的数学

在人类社会的实际操作上，数学甚至和工业工程相似。

例如没有研究过EGA细节的人也可能可以将其当作黑箱去发展stack上的代数几何，就像某个工厂的设备可以生产某种原料以供下一步生产；但是这个工厂的设备、流程等都不可复现了。很多技术手册因为年代久远，看似完整记录全部制作工艺，实际上是无法参考的，就像美国无法重造土星五号一样。
数学论文也是类似的，很多定理来自某个古代的论文，只有影印版且符号系统完全不同，还有很多不加定义的那个时代的约定俗成，或者根本找不到原始论文，而且这个过程还是递归的。

回到形式主义

有一些人尝试搞形式化证明，陶哲轩就搞Lean语言做数学形式化证明，用计算机验证逻辑正确性。这需要把论文的自然语言转写成基础逻辑的语言。这也许只在理论上是可行的。
但很明显这样依然需要验证代码的正确性，类似于机器证明四色定理。想要debug的话，可以使用相应的代码工具，但是这些代码工具同样可能有错误，这很容易引出无穷后退的问题。
写过代码的当然知道，即使测试样例足够多，在某些边界条件下程序依然可能出现非预期的行为。而且这样庞大的代码量必然不可能由某一个人全部完成，我们又一次依赖于信任其他人的工作。

悲观的前景

不幸的是，在科学中总是能够用做实验的方法找到错误，而在数学中似乎没有相应的手段。也许在这个领域里，数学研究的结果也只是“够用”的正确。说实话这挺让我不安的，但似乎也没什么办法，而且甚至寄希望于这种草台班子特性来让我的垃圾论文得以发表。