《基于 设计 bug 的证明过程》
还有 bug
坏了，定理证明器本身没有被形式化验证的问题终于从预想变为现实了^-^
看来以后人类的检查仍然在很长一段时间被需要。
我想起了某学校百米成绩破记录 然后一看100m跑道其实只有80m
不是能力强 是有bug。。。
