数学家借助 AI 证明几何猜想，发现无限族罗曼努金恒等式

埃默里大学博士后黄一峰与合作者提出并证明了 HJO 猜想，发现历史上的罗曼努金恒等式对应空间中的三叶结，并据此推导出无限族此前未知的恒等式。团队联合 Axiom Math 的数学专用 AI 系统 AxiomProver 协作探索证明思路，并将完整证明转译为 Lean 交互式定理证明语言进行机器验证。相关成果已作为预印本发表于 arXiv，为纽结理论、代数几何与数论的交叉研究开辟了新方向。