学习 AI 数学推理、定理证明与 Lean 形式化，适合数学和形式化方法爱好者。
15 条精选 · 入门 3 · 按推荐学习顺序：越基础、直观越靠前，越系统、深入越靠后
AI Is Getting Good at Math. Here’s Why.
文章列举了 2026 年一系列 AI 数学成果：OpenAI 内部模型找到 Erdős 单位距离猜想的反例、发表 Cycle Double Cover 证明、解决另外十个开放问题、给出 Navier-Stokes 证明；Anthropic 发布费马大定理形式化及黎曼猜想的新界。作者提出能否预测模型会解决哪类问题的议题，用“若干提示/洞见加上其间的努力”这一心智模型衡量问题复杂度，并引述 WT Gowers 对单位距离证明的评论。关注 AI 数学推理能力与问题难度分析的读者可读。
An OpenAI model has disproved a central conjecture in discrete geometry
这是 OpenAI 于 2026 年 5 月 20 日发布的文章，介绍一个内部 OpenAI 模型在平面单位距离问题上取得突破。该问题由 Paul Erdős 于 1946 年提出，问的是在平面放置 n 个点时最多有多少对点恰好相距 1。文中称，长期以来人们认为“方格”构造基本最优，而该模型推翻了这一猜想，给出了一族无穷多的构造，文章将其称为 AI 驱动数学的一个里程碑。
Mathematics Just Changed Forever — Kevin Hartnett
这是一个围绕 Kevin Hartnett 著作《The Proof in the Code》制作的纪录片式访谈视频。内容从 1998 年 Thomas Hales 计算机辅助证明开普勒猜想、Annals of Mathematics 无法判定其正确性讲起，讲述 Lean 从微软研究院的副项目发展为数学界用于校验证明的系统，并采访了 Lean 创建者 Leonardo de Moura、Jeremy Avigad、Kevin Buzzard 等人。后半部分转向 AI，涉及 AlphaProof、自然语言奥赛证明、自动形式化，以及“形式化鸿沟”这一概念。
Working with academic communities to build scientific understanding
OpenAI 发布的一篇研究类文章，介绍其在 Kakeya 猜想、指数时间假设（ETH）和量子色动力学等数学与物理问题上给出的模型结果，以及研究者如何验证并在此基础上继续工作。页面以“局部光滑化与 Kakeya 猜想”等小节组织内容。
这是一条 X 帖子，Scott Armstrong 用引用推文回应一条他无法回复的讨论串，评论 OpenAI 一篇流体 PDE 论文的构造，认为其与凸积分关系更大：凸积分中振荡通常靠手工构造、迭代产生病态弱解，而该论文巧妙设计了一种流体不稳定性，让流动自身从背景剪切中吸取能量产生振荡，雷诺应力则成为造出坍缩光滑涡的力。他指出用物理不稳定性制造应力没有先例，使之得到光滑而非粗糙的力，并提到相关想法部分见于 Leibovich–Stewartson 1983 等文献，但组合方式前所未见，也无人提出凸积分会参与此类爆破解。适合研究流体 PDE、凸积分与数学分析的人关注。
Leanstral 1.5: Proof Abundance for All
Mistral 发布的 Lean 4 形式化证明模型 Leanstral 1.5，采用 Apache-2.0 许可，总参数 119B、激活参数 6B。文中称其在形式验证任务上有大幅提升：miniF2F 达到饱和，PutnamBench 解决 587/672 题，FATE-H 达 87%、FATE-X 达 34%；训练经过中期训练、监督微调与基于 CISPO 的强化学习，并在测试的 57 个代码仓库中发现 5 个此前未知的缺陷。模型已开源，可通过 Hugging Face 和免费 API 使用。
这是 UC Berkeley EECS 127/227A 2026 年春季课程主页。页面提供本学期、2024 年春季和 2022 年秋季的讲座录像链接（不同学期内容并非互相覆盖），以及由往届教学团队编写、本学期将持续更新的课程讲义。阅读材料标注使用两本教材的缩写：CEG 指 Calafiore 与 El Ghaoui 的《Optimization Models》，BV 指 Boyd 与 Vandenberghe 的《Convex Optimization》。页面还链接了线性代数复习课幻灯片，并给出课程日历，第 1–2 周内容涉及最小二乘、向量范数、Gram-Schmidt/QR 与最小范数解等，另附讨论课题目与解答 PDF。适合想了解优化模型课程进度与配套资料的人阅读。
这是斯坦福 EE364A（与 CME364a 等同）的课程主页，页面注明基本课程信息在此，详细更新内容在 Ed 平台。课程在 2025–2026 夏季学期由 Logan Bell 和 Nikhil Devanathan 讲授，每周二、周四 12:00–14:00 在 Skilling Auditorium 上课，首次课为 6 月 23 日，第一周答疑需邮件预约，课程通过 CGOE 平台向注册学生提供录像；因讲座有录像，允许与同期其他课程同时选修，期末考试另设时间。页面还提供完整幻灯片 PDF、CVXPY 教程及若干凸优化应用示例链接，并列出课程助教。适合想了解凸优化入门课程安排和学习资源的人阅读。
这是斯坦福 EE364B（与 CME364b 等同，最初由 Stephen Boyd 开设）2026 年春季课程主页，主讲为 Mert Pilanci。公告称首次课在周一 30 日 1:30–2:50 于 CODA B90 进行，讲座录像提供给已注册学生。课程描述说明它是 364A 的延续，内容涵盖次梯度、割平面与椭球法，基于原始-对偶分解的分布式凸优化，单调算子与近端方法、ADMM，利用问题结构的实现，困难问题的凸松弛，分支定界全局优化，鲁棒与随机优化，非凸启发式，以及神经网络、扩散模型和蒙特卡洛采样的凸表述，并应用于控制、电路设计、信号处理、机器学习和通信等领域，以最终项目收尾；先修课为 EE364a。适合已学过凸优化基础、想了解进阶凸优化内容的人阅读。
MIT OpenCourseWare 上 6.231《Dynamic Programming and Stochastic Control》的讲义幻灯片页面，课程由 Dimitri Bertsekas 教授讲授，属电子工程与计算机科学系研究生课程，2015 年秋季开设。页面提供完整讲义 PDF 及分讲次幻灯片，例如有限时域问题讲座涵盖动态规划导论与示例、反馈的意义、最优性原理与通用动态规划算法、状态增广、确定性有限状态问题与逆向最短路径等。课程材料还包括考试及解答、习题集和视频。适合学习动态规划与随机控制理论的人使用。
这是 MIT OpenCourseWare 上 2014 年秋季开设的研究生课程 6.438 的课程页面，由电子工程与计算机科学系的 Devavrat Shah 教授讲授。课程介绍称其是研究生层次的统计推断原理入门，所涉概率模型以图表示方式定义，内容构成机器学习、信号处理、人工智能、计算机视觉与控制等方向工作的共同基础。页面列出课程所属主题（算法与数据结构、概率与统计、可视化等）以及可用资源类型，包括讲义笔记、习题集和考试。适合具备概率统计基础、希望系统学习图模型统计推断的研究生或相关方向学习者查看。
Signature Methods in Finance
DOAB 收录的开放获取图书，作者为 Christian Bayer、Goncalo dos Reis、Blanka Horvath、Harald Oberhauser，Springer Nature 出版，出版年份 2026，DOI 为 10.1007/978-3-031-97239-3，可免费合法阅读。简介称本书为路径签名方法这一快速发展领域提供入门指引，面向早期职业研究者和量化分析师、应用研究者等具备量化背景的从业者，涵盖近期进展并含编码示例；主题包括路径签名方法、机器学习、数学金融建模，以及交易、模型校准和统计金融中的示例。信源不提供版次。
LLMs are making formal software verification feasible at a much larger scale
Anthropic 的一篇研究文章，介绍其与 Theorem 合作，用 Claude 在 100 多个真实开源软件库的汇编代码（RISC-V）层面证明安全属性，并称过程中发现了多年未被察觉的缺陷。文章称这据其所知是首次在汇编层面把形式化验证大规模应用于生产软件。作者署名包括 Keane Lucas、Nicholas Carlini 等人。
Show HN: A proof-of-concept formalization of the IRS federal tax forms
这是一个 GitHub 仓库，作者称其全部由 AI 生成（vibe coded），目标是为美国联邦税表建立可追溯的形式化模型，让用户和维护者能把各项断言与解释回溯到权威原始文档，以解决此类软件可信度依赖维护方的问题。作者明确表示项目目前处于搁置状态，不应作实际用途。适合对税务软件形式化、可验证软件与 AI 生成代码可信度话题感兴趣的人阅读。
AI-assisted proof of optimal packing for 11 squares
一个 GitHub 仓库，包含 11 个正方形装箱最优性证明的 Lean 形式化版本。据 README，完整证明已在 EvolvingPrograms 的验证运行中通过，涉及 7,920 个本地 Lean 模块，最终审计报告零处 admitted；部分精确数值证书检查使用 native_decide，几何、检查器可靠性与证明组装仍用普通 Lean 证明。最优边长由含八次方程根 u 的公式给出，数值约为 3.8770835900228141773，并附有验证报告与证书哈希记录文件。