[3/3] 终于完成了圣诞节至今卡住的一个阶段性工作,提交了将近 2000 行新代码——其中一半是在国内期间完成的。现在导师已经相信这个工作的难度前所未有了,因为我已经把他之前的相关代码量给翻倍了,而且我遇到的几乎每个新定理的证明都超长。试用期肯定没问题了,下周开始我要教书了(讲 HOL 定理证明器用法和形式化概率论)。
[3/3] 终于完成了圣诞节至今卡住的一个阶段性工作,提交了将近 2000 行新代码——其中一半是在国内期间完成的。现在导师已经相信这个工作的难度前所未有了,因为我已经把他之前的相关代码量给翻倍了,而且我遇到的几乎每个新定理的证明都超长。试用期肯定没问题了,下周开始我要教书了(讲 HOL 定理证明器用法和形式化概率论)。
No replies yet.