Farhi, Goldstone and Gutmann

AI与Lean 4合作完成量子优化证明

研究人员利用大型语言模型Claude Fable 5和Lean 4证明助手，成功解决了量子优化领域一个存在十年的猜想。该猜想由Farhi、Goldstone和Gutmann提出，涉及量子近似优化算法（QAOA）在环形图上的近似比。研究方法包括在Lean库中形式化问题，然后让LLM构建证明，并由Lean进行验证。此方法揭示了一个隐藏的动力学对称性，并利用了相邻领域的工具，展示了AI推理与形式验证在科学发现中的强大协同作用。