田春冰河
2020-01-10 19:08:52 发布
[1/3] 话说前天我提交给 HOL 官方的 400 多行代码——就是我跟大小老板合写的论文里某定理的形式化版本——已经顺利被合并了。这样我在 HOL 贡献者排名里按照新增代码行数还差不到一千行就可以晋级了。结果没想到给 HOL 提交 PR 比正式发表论文还管用，排名第二的 Konrad Slind，一个比我早学定理证明 ...全文