Wiki 知识库

全部文档 / 标签: 自动定理证明

2 篇
清除

全面解读孙宇晨奖及如何参与拿到最高100万美元奖金

孙宇晨设立数学奖,单题奖金最高100万美元,采用机器可验证的Lean形式化证明作为评判标准,去中心化、零信任地取代传统评奖委员会。作者认为这对个人和小团队是重大机遇:奖项不设门槛,且30%奖金专门留给形式化工作,即把已有公开证明搬进Lean即可拿钱。作者分析了三种参与方式(全做、只做形式化、只出思路),推荐小团队从形式化切入,并给出三人团队配置建议、官方入口和Lean工具链教程。作者认为该奖项将倒逼AI行业从'看起来对'转向可复查的可靠推理,带来结构性利好。

技术 › LLM Captain Kent | 肯特船长 2026-09-166.1 KB 77

数学照妖镜:AI 能发现新的数学定理吗?

文章回顾了人工智能与数学证明的深厚渊源,从1950年代的Logic Theorist到哥德尔不完备性定理,探讨了形式化数学的演进。重点介绍了现代AI数学的基础设施LEAN(包括其核心人物Leonardo de Moura、从v3到v4的演进及mathlib库),以及DeepMind、Harmonic、Axiom Math等科技巨头和初创公司在AI自动定理证明领域的布局。文章指出,AI正在通过神经网络与形式化验证的结合,重新回归逻辑推理的起点。

技术 › LLM snowboat 2026-05-0760.9 KB 11.4K 16 76