[2/3] 也许有人觉得形式化（数学）证明就是把书上的证明过程在定理证明器里换个语法抄一遍，就是个纯工程性的行为谈不上科研，那你可能是对的但经常是错的。那些书面证明要真是 “完全正确的”，运气好的话连语法都不用改，真的可以逐行抄下去，但你未必有这种 “运气”。比如图1是中心极限定理某个版本证明过程中的一个很小的引理，红框里正在对一个带有参数的积分求（高阶）导数，可以想象写这个证明的人直接一笔带过就没怀疑过这么做的可行性（事实上这一步也是正确的），但问题是在一般情况下对积分号进行求导需要满足严苛的条件，一篇论文显示来自柯西本人（微积分严密性）的积分表里就有两个这样的错误公式（说是相等但其实是发散的），被无数编造积分表的作者盲目抄袭，直到 185 年后的 2000 年才被人发现是错的。我也是运气不好（但也可以说是运气好，因为论文里有得说了），偏偏就遇到了这个问题。为了形式化证明图1红框里那一步，花了至少五千行形式化代码（和三个月）的代价。纸面上可以糊弄过去的地方，定理证明器可不惯病，逻辑上差一点儿都不行。