暂缓
三年前
校招季得不到认可
价值观受到冲击
事情的进展和预想的完全不同
我陷入了迷茫
机械化
”适应社会的游戏规则，往上爬“，我无法接受这样的一生
我信奉，“人生的意义在于创造价值”
工作实现的价值太小，一直以来我给自己的期望很高
我不停地思考，希望能有机会做出些什么
适逢吴文俊院士逝世一周年，想起自己对机器证明的兴趣，开始学习几何机械化理论
我大致理解了吴老的方法
很巧妙，但不是我想要的，这样的机械化不能启发人思考
有没有可能把人的证明机械化
如果能行，无疑会有更大的价值
初衷
一开始我准备做一个欧式几何的证明机器，和人的证明方式一致，不依赖计算机的强大运算能力
我很快意识到问题的难点在于如何表达数学问题
我对点，线分别建立类，然后依赖点，线作为输入，建立角，三角形的类；
对线段，角相等，赋值分别建立类，对平行，垂直关系建立类。
完成了一个很迷你的表示系统。
也就是用类去表达基础的数学概念和数学关系。
另一个问题是自动推理的问题，也就是定理的触发。
调研发现很多研究有尝试的过程，被指数爆炸击败。
我不断思考我自己解题的时候是怎么想的，为什么人脑不会指数爆炸。
最后我提炼出一个准则，即定理作为概念的属性，由概念的状态触发。
第一版自动推理系统，尽管简陋，却让我看到无限的可能。
符号计算
线段角度的计算很快出现三角函数，勾股定理相关的计算。
很多问题是披着几何外衣的代数问题。
我决定直接上手搭建符号计算系统，像 mathematica 一样。
简单调研之后发现了 sympy 这个符号计算包，和我之前的思路是一致的。
用类去表示基础概念如变量，基础关系如加法。
我认识到概念先于定理可能是我独特的想法。
准备搭建一个解决线性代数问题的系统，测试用例用北大教材的习题。
理论基础
mathematica 对矩阵向量的支持很有限，不支持带变量维度的矩阵，如 \(\{a_{ij}\}_ {m\times n}\)
我做到了，我把前三章的习题，除了少数几道，都自动化了。
分类讨论，变量赋值，不等式约束，不断引入新的东西。
代码开始变得很臃肿，加入新特性的代价越来越大。
我的方法局限性太大了。
我需要建立一套理论，用理论来指导代码，规范代码。
巨人的肩膀
面对象编程，编译原理，类型系统，形式证明，图灵，丘奇，……
在理解前人的理论的同时，我脑子里一些模糊的想法清晰了起来
图灵机对应莱布尼茨的设想，问题的关键有两点：编码 和 转换
丘奇的理论表明，所有编码问题可以归结为 复合 与 抽象
复合，函数，类型系统，面对象编程，是一体的
prototype-based 比 class-based 更一般
我不断重塑我的系统，分三个方向：
- 用抽象与复合的方式建立符号体系。
- 搭建类型系统（类比prototype，类型与符号不做区分）。
- 搭建解析器，语言采用数学语法（而非程序语法）。
转换采用流的思想，所有状态按有序的方式转化。
不同
理解了这些就能理解学术界，工业界，和我的不同。
目前的形式证明系统如lean，基于丘奇的lambda calculus，丢失了复合的边界。
目前的复合计算软件如mathematica，对抽象做得不够彻底。
这是在编码上，最本质的不同在转化上。
系统的思路模拟人的思路，这是最高的指导思想，也是最朴素的。
自动推理不是去找一个通用的解决问题的方法，而是去深入理解前人的思想，然后翻译给计算机执行。
这比听上去困难许多。
路漫漫
三年过去了，类型系统和解析器都还有很多内容需要填补。
赋值传导逻辑，等式不等式化简逻辑，加法乘法逻辑，lambda表达式逻辑……
还有一系列的问题需要解决和发现。
最近身体出了不小的问题，调理了近三个月才好了一些。
理想的压力，工作的压力，生活的压力，让我的神经崩溃了。
计划用十年完成一个初步成熟的系统，现在看来还是太心急了。
用三十年吧。
把身体放在第一位，等生活安顿下来，换一个压力小一点的工作。
虽然计划可能会停滞很长一段时间，没有关系。
我要尽可能地延长自己的职业生涯，才有可能完成这个计划。
说起来我一开始做这个系统，就是希望把竞技体育的优点引入学术研究。
诸如科学系统的方法，不同水平选手都能参与的分级制度。
就当是退出这个赛季，会有复出的那一天。