AI解决图论中20年未解猜想
研究人员利用AI（Lean证明助手）证明了一个20年历史的图论猜想：在半流式匹配中，贪心算法达到了最优近似比。这一结果被形式化验证，展示了AI在数学证明中的潜力。
在计算机科学和数学的交叉领域，一项跨越20年的图论猜想近日被人工智能辅助证明所攻克。研究人员宣布，他们严格证明了在半流式（semi-streaming）匹配问题中，贪心算法能够达到最优的近似比。
该成果由Sepehr Assadi、@mangooqwq以及一位合作者共同完成。他们不仅给出了一个简洁的10行算法，还使用Lean证明助手对其进行了形式化验证，确保了推理的严谨性。半流式匹配是处理大规模图数据的关键技术，这一结果意味着贪心策略在实践中是最优选择。
Lean是一种交互式定理证明器，它允许数学家以计算机可检查的方式编写证明。此次成功表明，AI可以协助解决长期以来悬而未决的难题，为未来的数学发现开辟了新路径。相关论文已发布在arXiv上，代码和证明也已公开。