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