我在人生的第五十个年头，fundamentally的改变了对数学的看法。证明论是革命性的。很多人耳熟能详的牛逼人物比如希尔伯特，图灵或丘奇，旷世奇才哥德尔和塔斯基，其实都没有根芩，Prawitz，Per Martin Lof（这位是Kolmogorov的学生）等人对证明论的推动力度大。
++++
逻辑学的一个极其powerful的工具就是可以用一个复杂的predicate表达一个property，包含嵌套的条件和量词甚至是高阶逻辑。我不相信任何人能离开这种形式化工具能「直觉」的把property在inductive定义的数学对象上证明下去。
如果你有定理证明器，这种证明可以象程序一样run，如果没有，使用一些规范化的书写方式也很容易在纸上把这个过程变得平顺易读，而不是感觉大脑里存储context变量和临时proposition的空间耗尽了。
我相信很多伟大的数学天生神力天赋禀异，但我也相信没有人的力气能超过火车，没有人的速度可以快过芯片。
++++
我们正在经历的这个时代，无论ai还是自动定理证明，本质都是一个，就是思维可以机械化了。