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