在計算機科學和數學的交叉領域，一項跨越20年的圖論猜想近日被人工智能輔助證明所攻克。研究人員宣佈，他們嚴格證明了在半流式（semi-streaming）匹配問題中，貪心算法能夠達到最優的近似比。
該成果由Sepehr Assadi、@mangooqwq以及一位合作者共同完成。他們不僅給出了一個簡潔的10行算法，還使用Lean證明助手對其進行了形式化驗證，確保了推理的嚴謹性。半流式匹配是處理大規模圖數據的關鍵技術，這一結果意味着貪心策略在實踐中是最優選擇。
Lean是一種交互式定理證明器，它允許數學家以計算機可檢查的方式編寫證明。此次成功表明，AI可以協助解決長期以來懸而未決的難題，為未來的數學發現開闢了新路徑。相關論文已發佈在arXiv上，代碼和證明也已公開。