午夜#学术新闻#

GitHub 仓库 Pengbinghui/pipeline-math 是一个数学研究与自动化证明相关的项目。它收集并尝试解决一些数学领域的开放问题，包括：

COLT（计算学习理论会议）的开放问题；

交换环论（commutative ring theory）中的经典难题；

Erdős（保罗·埃尔德什）提出的问题；

FOCS 2023论文中的开放问题。

使用 GPT-5.5 Pro 通过一个 “证明–验证”流水线（prover–verifier pipeline）来生成证明。

论文初稿由 Claude Code 组装，再由作者团队润色和验证。

在 Lean 4 中对交换环论的解答进行形式化验证，利用自动化的 Lean formalization pipeline。

它解决了 9 个具有挑战性的开放问题，包括来自著名理论计算机科学会议的开放问题——COLT 开放问题列表中的 4 个和 FOCS 中的 1 个——以及交换代数中的 4 个问题。

COLT开放题目：
• 洗牌SGD — SS–RS–GD不等式（Yun， Sra， Jadbabaie， COLT 2021）
• 稳健条件概率估计（Langford， COLT 2010）
• 学习测量输出量子电路（Kun & Reyzin，COLT 2015）——部分解法
• 线性回归的无加权数据选择，问题3（Hanneke， Moran， Shlimovich， Yehudayoff， COLT 2025）

交换代数中的4个未解问题（由Cahen–Fontana–Frisch–Glaz提出的交换环论中的未解问题）

2026年6月28日：新增了 Erdős Problem 477 的解答。

http://t.cn/AXoAvKmx