AI 把数值分析直觉直接变 Lean 硬证明，误差界证到 10⁻⁴⁸
geoffreyirving · x · 2026-10-15
Geoffrey Irving 展示了一个具体成果：exp 函数的三倍精度（triple-double）展开逼近的 Lean 形式化证明，误差界为 |exp x − eˣ| ≤ (17/16·u³ + 2⁻¹⁶²)·eˣ + 3η ≈ 1.63×10⁻⁴⁸，其中 u = 2⁻⁵³、η = 2⁻¹⁰⁷⁵；另含多个超越函数及来自全纯动力学的例子。
结合其上文：过去这类 IEEE 浮点误差严格界定论文需要大量时间，如今「只要有 Rough 的理论直觉，AI 就能把它翻译成硬理论」，数值分析与严格证明之间的差距几乎被抹平，所需工作量极小。
「研究」频道最新
- 数据量决定智能边界：按数据排序后锯齿前沿变螺旋 — sebkrier · 2026-10-16
- Doc2Harness 基准：19 个前沿模型测编码 Agent，最高通过率仅 53% — _akhaliq · 2026-10-16
- 李飞飞团队开源 OpenWAM：统一世界-动作模型框架，让机器人视频预训练成大脑 — jiqizhixin · 2026-10-16
- NVIDIA TacitVLA：动作不读思维链，推理收益保留、延迟最高降 3.4 倍 — arankomatsuzaki · 2026-10-16
- Cohere Labs 世界模型公开课第 4 期：一文理清 DreamerV1-V4 架构演进 — Cohere_Labs · 2026-10-16
- GPT-6.1 审查 arXiv：6% 论文主定理有错，近两月降至 1.5% — nitarshan · 2026-10-16