《数学原理》重写工程——该项目致力于将罗素与怀特海的《数学原理》使用 Coq 语言完全重写，补全原书的逻辑漏洞，将其中的证明进行 100% 的机器形式化验证。同时，项目还会将 Coq 的证明进行排版，生成和原书风格一致、可检索、排版精致的文本供人类阅读。所有代码将以自由软件许可证发布在 GitHub 上。http://t.cn/A6xOOy08 记得我去年因好奇，还专门查过有没有人用机器检查过《数学原理》中的证明，结果居然没有。现在终于有人开始做了，佩服！