全部文档 / 标签: 数学证明

2 篇

生成越来越便宜，验证越来越贵 | 峰会洞察 01

作者记录硅谷101 Alignment 2026 年度峰会 Day 1 三场分享的核心洞察：模型竞赛、新型AI研究实验室与AI for Science。贯穿全场的主题是'生成越来越便宜，验证越来越贵'。开源vs闭源之争本质是利润表问题，价值向model-agnostic应用层转移；数学因可验证、可数字化、数据充足成为AI攻克焦点，验证成本趋近于零是北极星；AI for Science最大瓶颈是湿实验验证周转时间。作者从投资视角提出：拆解AI应用公司COGS、关注闭源转开源迁移路线图、可验证代码生成是下一个基础设施层。

技术 › LLM

Cloris 2026-10-1224.0 KB 18.1K 40 87

AI峰会开源模型闭源模型验证成本 AI for Science 数学证明 RSI 投资框架模型竞赛可验证代码

数学照妖镜：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

AI 数学证明 LEAN DeepMind 逻辑推理形式化验证 Axiom Math mathlib 科技史自动定理证明