一篇 Hacker News 帖子链接到一篇题为“如何形式化全部数学”的文章。评论区争论哥德尔不完备定理和 Chaitin 的思想是否对这种项目构成挑战。一位评论者认为这些反对意见无关紧要，因为该项目针对的是已有自然语言证明的已证定理，而非所有可能的定理；如果某个现有定理无法被形式化，其原始证明可能有缺陷。另一位评论者持更怀疑、更哲学的观点，认为数学是无尽生成的，长期形式化框架可能类似于空洞的宗教信念。其他评论拿历史先例开玩笑，提到了朗兰兹纲领和《数学原理》。页面还包括标准的 Hacker News 导航和 Y Combinator 申请通知。