★ 5
AI 生成纳维-斯托克斯千禧难题解答
OpenAI 分享了一份由 AI 生成的纳维-斯托克斯千禧年大奖难题解答，包含文字说明与 Lean 形式化证明。该成果若成立将是数学界重大突破，但也引发对证明有效性的广泛质疑与讨论。
OpenAI55 天前
#Lean
共 18 篇相关资讯，按重要度与时间排序，每 3 小时更新。
★ 4
OpenAI 称其 AI 在 Lean 中证伪指数时间假设
有报道称 OpenAI 的 AI 系统在 Lean 证明助手中给出了指数时间假设（ETH）的反证，若成立将是计算复杂性理论的重大突破。该说法目前仅见于单一来源，尚待数学界与形式化验证社区核实。
Hacker News – AI5 天前
★ 4
基于 Gemini 的智能体在忙碌海狸 BB(6) 自主发现并形式化验证加速规则
论文构建基于 Gemini 的智能体流水线，整合模式识别、自动猜想、非形式数学推理与 Lean 形式定理证明，在不可计算的忙碌海狸 BB(6) 领域自主发现并形式化验证了 11 台图灵机的新型 Collatz 式加速规则。这些机器暂被归类为 Cryptids，展示了 AI 在开放式数学发现中的潜力。
arXiv cs.AI13 天前
★ 4
OpenAI 数学项目据称证明 Barnette 猜想引热议
Hacker News 用户 Jake Boggan 评论称，自己钻研 24 年的 Barnette 猜想似乎已被 OpenAI 的 math 项目（problem 180）证明。他表达了复杂情绪，称投入数千小时的问题被解决让他感到怅然。该讨论反映 AI 攻克数学难题对研究者心理的冲击。
Simon Willison Blog26 天前
★ 4
OpenAI 发布前沿大模型全新数学能力测试成果
OpenAI 通过 GitHub 代码库公开其内部前沿大模型生成的一系列全新数学研究成果，并附带论文修订与引用的规范协议。成果包含 Lean 语言形式化证明，可让数学证明直接通过计算机校验。单份成果平均消耗算力约等于 ChatGPT Pro 三小时深度推理时长。
36氪26 天前
★ 4
Magenta：打通数学推理与Lean形式化验证的闭环
论文提出Magenta，一个免训练的智能体流水线，仅给定自然语言问题即可产出答案、将其表达为Lean 4命题并构造机器可验证的证明。系统包含命题裁判以验证形式化是否保留原问题，以及错误归因裁判将失败尝试路由到数学重新推导或局部Lean修复。Magenta在AIME 2025、AIME 2026和H…
arXiv cs.AI51 天前
★ 3
EasyProver：递归智能体Lean证明系统解出669/672 PutnamBench
论文提出EasyProver，由隔离上下文的递归智能体、异步搜索、并行策略探测与弹性精化服务构成，无需额外训练即解出669/672道PutnamBench题与全部6道IMO 2026形式化题。团队同时发布Aegis基准，将竞赛编程题转为真实实现上的Lean验证任务，EasyProver在2000条…
arXiv NLP3 天前
★ 3
PaperFormalizer 推出 Lean 论文形式化作者在环流水线
研究团队发布 PaperFormalizer，一个基于 Lean 的智能体流水线，从 LaTeX 源码出发将论文转写为陈述依赖图，审计忠实性与歧义，再在 Mathlib 上形式化并证明。流水线在陈述存在多种解读时暂停询问作者，输出带注释的修订版论文、变更报告与 Lean 代码，可运行于 Claud…
arXiv cs.AI7 天前
★ 3
数学博主 Karagila 称不信任 AI 生成的 Lean 代码
数学博主 Asaf Karagila 发表文章，表示不信任 AI 生成的 Lean 形式化证明代码。文章讨论了 AI 在数学证明辅助工具中的可靠性问题，引发对 AI 生成形式化代码可信度的关注。
Hacker News – AI22 天前
★ 3
陶哲轩撰文谈 Lean 定理证明器的可靠性与 AI
数学家陶哲轩在其博客发文，向数学界介绍 Lean 定理证明器，重点讨论其可靠性问题以及与 AI 的结合。文章探讨了形式化证明工具在数学研究中的价值，以及 AI 辅助证明带来的可信度挑战。
Hacker News – AI23 天前
★ 3
Choir：分布式多智能体形式化开放协议
当前用 Lean 等证明助手形式化教科书与定理的工作多为集中式，由单一团队承担全部算力成本。Choir 提出开放协议，将项目拆解为可由独立贡献者完成的任务，各自运行自己的智能体与 LLM 订阅，通过 GitHub 仓库协调，合并前经确定性门禁校验。协议支持 Lean 4、Isabelle 与 Ro…
arXiv cs.AI34 天前
★ 3
数学中 AI 的错位：Kevin Buzzard 回应
数学家 Kevin Buzzard 在 Lean 社区回应了关于 AI 在数学领域存在严重错位的讨论。该对话聚焦 AI 形式化证明与数学研究实践之间的偏差，引发学界关注。
Hacker News – AI50 天前
★ 3
ProofEvolve：神经符号进化自动定理证明
ProofEvolve结合神经模型和符号Lean内核，通过进化机制扩展证明知识边界。它利用行为索引档案和模式库，保留部分证明成果，在多个Lean基准上取得最高平均求解率，展示了递归自改进的潜力。
arXiv cs.AI66 天前
★ 3
FaithSieve：细粒度数学证明评估框架
FaithSieve利用Lean辅助验证自然语言数学证明，通过分解证明步骤和语义对齐评分，实现精确的错误定位。在奥林匹克和大学级数据集上，其准确率显著优于直接判断基线，展示了形式化证据在评估中的价值。
arXiv cs.AI66 天前
★ 2
Lean 创造者 Leo de Moura 谈 AI 与形式化验证的未来
Lean 创造者 Leo de Moura 在访谈中讨论 AI 与形式化验证的结合前景，探讨大模型在数学证明与程序验证中的角色。该话题在 Hacker News 引发小范围关注。
Hacker News3 天前
★ 2
RefactorProof 基准：代码重构后 LLM 生成证明稳定性测试
论文提出 RefactorProof，从 VERINA 任务派生 458 个 Lean 认证变体，检验程序重构后证明是否仍有效。结果显示专用证明器（DeepSeek-Prover-V2-7B、Goedel-Prover-V2）的未改动证明存活率反而高于参考证明，但失败不等于修复成本高。
arXiv cs.AI5 天前
★ 2
研究揭示 Lean 定理证明中验证器反馈的「事后代价」
论文在 Lean 定理证明中做受控单步实验，考察展示失败证明、编译器错误与重试指令对自我修复的影响。结果显示展示失败前作会降低成功率并加剧抄袭，而正确诊断信息本身并不优于错误诊断对照。在 Qwen3.6-27B 与 DeepSeek-Prover-V2-7B 上，没有任何反馈条件能超过纯指令重采样。
arXiv cs.AI13 天前
★ 2
Lean Pool：AI维护的形式化数学档案库
Lean Pool是一个形式化数学仓库，由AI智能体负责其增长、维护与优化。该工作展示了AI智能体在形式化数学知识库长期自主运营上的应用方向。
arXiv cs.AI40 天前