自动定理证明 LLM-DailyDigest 2026-08-30 2026-08-30 约 100 字 预计阅读 1 分钟 自动定理证明 本主题由提交工具自动创建，可在此补充洞察与资料。 相关消息（按子主题自动聚合） 反例搜索 1 Gowers：AI数学突破更擅长搜索反例与特殊构造 08-17 多智能体系统 1 Cogentic：面向自动化证明发现的多智能体编排框架 10-01 形式化证明 35 数十个 AI Agent 24 天形式化有限单群分类定理 10-29 智能体算法设计：在 Lean 中提出、形式化并证明进化算法运行时界 10-27 微软研究员借助 AI 证明 KLS 猜想 10-22 OpenAI纳维-斯托克斯证明路线遭重新解读 10-18 AlphaProof Nexus攻克9项埃尔德什问题并证明44项OEIS猜想 10-18 LeanGraphSearch：面向形式化定理证明的图搜索 10-18 面向 GPU 高效证明候选评估的 Lean 反馈学习 10-18 AI批量攻克数学难题引发“数学末日”争议 10-10 报道称OpenAI用万名智能体攻关千禧年数学难题 10-10 NanoProof：开放高效的 Lean 4 自动定理证明器 10-10 LEVER：基于 AND/OR 图的自适应成本感知证明搜索 10-09 Claude被曝以Lean证明渗流理论连续相变猜想 10-08 CoCo-Prover：智能体编排驱动的低成本程序定理证明 10-08 让方法库自荐：面向形式化证明的适用性感知方法选择 10-08 FYAN：面向文档级形式化的语义审计人机协作框架 10-01 ProofLoom：以证明义务驱动的随机优化理论自动形式化 09-30 AI辅助Lean完整形式化验证庞加莱猜想证明 09-29 报道称万名 AI 智能体用形式化证明攻克 Navier–Stokes 难题 09-25 Lean Pool：AI 维护的形式化数学档案库 09-24 GPT-6 Astra证明刘维尔–哥德巴赫猜想并经Lean 4验证 09-21 传OpenAI积压数百项AI生成数学证明 09-18 FormalFlow：MIP* = RE 核心定理的长程自动形式化 09-18 传 AI 巨头未公开数百项数学证明，真实性尚待确认 09-16 Aaronson称AI公司或暂未公开多项数学突破 09-16 OpenAI被曝逼近霍奇猜想，并与Anthropic竞逐BSD猜想 09-11 OpenAI称在第二道千禧年难题上取得实质性进展 09-11 Claude 11天完成费马大定理证明 09-07 Claude借助多智能体Harness完成费马大定理形式化证明 09-07 Claude 推进黎曼猜想零点界，获数学家重证与 Lean 验证 09-07 Claude多智能体形式化验证费马大定理 09-07 GPT-5.6提出大素数空隙新构造并通过Lean验证 09-07 AxQM：有限维量子力学形式化证明合成基准 09-07 Claude 以 Lean 完成费马大定理端到端形式化验证 09-07 AxiomProver用Lean 4完成“246定理”形式化验证 08-23 AI 辅助攻克森多夫猜想，陶哲轩推导出更强结果 08-16 形式化证明修复 1 CAPRI：面向 Isabelle 的契约感知证明修复 08-16 形式化评测 1 FormalTCS：端到端前沿理论计算机科研评测 08-21 形式化验证 1 AI 证明泛滥后，可信验证成为最昂贵的智能 08-19 数学发现 1 Claude辅助构造S⁶复结构，挑战78年数学悬案 08-26 数学推理 6 OpenAI公开三维与四维挂谷猜想证明手稿 10-10 数学家呼吁抵制 OpenAI 批量发布 AI 生成证明 10-09 未发布 Claude 推进黎曼猜想相关下界并支持形式化验证 10-08 OpenAI内部模型被曝24天攻克百余道数学难题 09-22 OpenAI以千禧年难题测试万级Agent数学研究系统 09-11 OpenAI被曝在霍奇猜想等数学难题上取得进展 09-11 模型评测 1 SIV：基于定理证明器的 NL→FOL 翻译评测指标 09-29 科研评测 1 TCSAlgBench：研究级理论计算机科学自动证明基准 09-30 策略蒸馏 1 SimpleOPD：分词器无关的长上下文同策略蒸馏 08-17 脚手架演化 1 面向 Rocq 与 Lean 的智能体证明器接口演化 10-01 自动化科学研究 1 OpenAI 公开 722 篇 AI 生成数学手稿 10-08 自我改进 1 回望式分层规划：通过事后提炼思路训练推理模型 10-09
