Hacker News 最新 | 过往 | 评论 | 提问 | 展示 | 招聘 | 提交 登录 我们是否被 Lean 困住了？ (mathoverflow.net) 12 点，作者：jjgreen，2 小时前 | 隐藏 | 过往 | 收藏 | 1 条评论 帮助 7373737373，20 分钟前 [–] Metamath 的 Python 验证器（其可信内核）仅需 700 行简短的 Python 代码：https://github.com/david-a-wheeler/mmverify.py/blob/master/m... Metamath Zero 的 Haskell 实现为 700 行，C 实现为 1000 行（总计 1800 行）：https://github.com/digama0/mm0 其他证明系统的对比情况如何？ 部分错误统计：https://tristan.st/blog/in_search_of_falsehood 回复 考虑申请 YC 2026 年秋季批次！申请截止日期为 7 月 27 日。 指导方针 | 常见问题 | 列表 | API | 安全 | 法律 | 申请 YC | 联系方式 搜索：