田春冰河
2019-09-26 19:57:58 发布
[1/3] 过去三天里我一鼓作气把 HOL Light 的形式化微积分给移植到 HOL4 里了。之前 HVG Concordia 的人打下了良好基础，但总共 700 多个定理中还有 30 多个无法完成，我从简单的开始逐个击破，只花了两天就全搞定了。我又给 HOL 提交了两万行代码，还在官方手册新增了一章 “高等数学”，等待审核。