★ 4
基于 Gemini 的智能体在忙碌海狸 BB(6) 自主发现并形式化验证加速规则
论文构建基于 Gemini 的智能体流水线，整合模式识别、自动猜想、非形式数学推理与 Lean 形式定理证明，在不可计算的忙碌海狸 BB(6) 领域自主发现并形式化验证了 11 台图灵机的新型 Collatz 式加速规则。这些机器暂被归类为 Cryptids，展示了 AI 在开放式数学发现中的潜力。
arXiv cs.AI13 天前
#定理证明
共 14 篇相关资讯，按重要度与时间排序，每 3 小时更新。
★ 4
Magenta：打通数学推理与Lean形式化验证的闭环
论文提出Magenta，一个免训练的智能体流水线，仅给定自然语言问题即可产出答案、将其表达为Lean 4命题并构造机器可验证的证明。系统包含命题裁判以验证形式化是否保留原问题，以及错误归因裁判将失败尝试路由到数学重新推导或局部Lean修复。Magenta在AIME 2025、AIME 2026和H…
arXiv cs.AI51 天前
★ 4
DeepSeek-Prover-V2开源定理证明模型
DeepSeek发布开源Lean 4定理证明模型Prover-V2，采用递归证明搜索和强化学习，在MiniF2F基准上取得顶尖成绩。
Synced 机器之心英文版550 天前
★ 3
EasyProver：递归智能体Lean证明系统解出669/672 PutnamBench
论文提出EasyProver，由隔离上下文的递归智能体、异步搜索、并行策略探测与弹性精化服务构成，无需额外训练即解出669/672道PutnamBench题与全部6道IMO 2026形式化题。团队同时发布Aegis基准，将竞赛编程题转为真实实现上的Lean验证任务，EasyProver在2000条…
arXiv NLP3 天前
★ 3
DRAGO：确定性诊断修复 LLM 生成形式化规格，回归率降至 1.3%
论文提出 DRAGO 修复框架，用确定性、形式化系统专属诊断替代无依据的 LLM 批评，仅在诊断错误权重严格下降时保留改写。在 SMT-LIB2、MiniZinc、PDDL 五个基准上，回归率从 11.8% 降至 1.3%，答案准确率较零样本形式化提升 12.9 个百分点。论文还发现 Planet…
arXiv cs.AI13 天前
★ 3
陶哲轩撰文谈 Lean 定理证明器的可靠性与 AI
数学家陶哲轩在其博客发文，向数学界介绍 Lean 定理证明器，重点讨论其可靠性问题以及与 AI 的结合。文章探讨了形式化证明工具在数学研究中的价值，以及 AI 辅助证明带来的可信度挑战。
Hacker News – AI23 天前
★ 3
研究提出统一几何状态下的密集神经符号推理
论文提出密集神经符号耦合框架，让神经引导与符号执行共享类型化状态，在每步搜索中通过可执行动作通信。实例化为OmniGeo统一求解平面、解析与立体几何，配合Claude Sonnet 4.6在FormalGeo7K等基准达90.8%宏平均，并解出IMO-AG-30中的21/30题。
arXiv cs.AI27 天前
★ 3
AI 是数学的终结吗
《量子杂志》文章探讨 AI 对数学研究范式的冲击，讨论机器能否参与定理证明与数学发现，以及这对数学学科意味着什么。属于深度思想报道，涉及 AI 与基础科学的交叉议题。
Hacker News – AI27 天前
★ 3
陶哲轩：强大AI模型对数学家意味着什么
数学家陶哲轩撰文探讨强大AI模型对数学研究的影响。他分析了AI在定理证明、猜想生成与协作研究中的潜力与局限，并呼吁数学界主动适应这一变革。该文为理解AI与基础科学的关系提供了权威视角。
Hacker News – AI29 天前
★ 3
研究：让大模型发现有趣数学定理
论文提出以「证明长度与命题长度之比」定义定理的内在趣味性，并证明其与下游实用性高度相关。作者训练了一个 27B 模型来预测给定前提下的证明难度，其准确度超过前沿通用模型。优化该指标后，模型生成的定理与 Mathlib 的重叠率从 91.9% 降至 30.6%，展示了构建自扩展、机器可验证数学库的路…
arXiv cs.LG38 天前
★ 3
LogicTrack：用形式逻辑求解器审计推理链
论文提出LogicTrack神经符号框架，将LLM的每一步推理自动形式化为符号表示，并用自动定理证明器验证，解决模型通过逻辑缺陷链得出正确答案的问题。框架引入基于求解器的回溯奖励（SBR）指导推理时树搜索，并可生成SFT数据让模型内化逐步审计能力。在8个推理基准、7个LLM上验证了推理链可验证性与…
arXiv cs.AI42 天前
★ 2
新方法用 Lean 4 编译器报错修复定理证明，解出率提升 32%
论文提出有界在线步骤级修复模块：每步采样 K 个策略，失败时把 Lean 4 编译器错误信息喂给预训练修复模型就地修正，而非丢弃重采样。在 LeanDojo 1990 条定理子集上最多取得 32% 相对提升、多解出 82 条定理，收益主要来自浅层策略执行错误。该方法在 Lean Workbook …
arXiv cs.AI12 天前
★ 2
研究揭示 Lean 定理证明中验证器反馈的「事后代价」
论文在 Lean 定理证明中做受控单步实验，考察展示失败证明、编译器错误与重试指令对自我修复的影响。结果显示展示失败前作会降低成功率并加剧抄袭，而正确诊断信息本身并不优于错误诊断对照。在 Qwen3.6-27B 与 DeepSeek-Prover-V2-7B 上，没有任何反馈条件能超过纯指令重采样。
arXiv cs.AI13 天前
★ 1
AI是否已永远改变数学？
一段由物理学家Brian Greene与数学家Tristan Buckmaster参与的讨论视频在Hacker News上被分享，探讨AI对数学研究范式的冲击。话题聚焦AI能否在定理证明、猜想发现等核心数学活动中带来根本性变革。目前讨论热度极低，属于小众学术圈话题。
Hacker News – AI28 天前