腾讯混元称Hyra找到关键构造，并公开论文、显式构造与Lean形式化证明。
推荐理由：关键不只是AI搜索出新构造，而是同时给出Lean形式化证明；这把AI数学发现从候选答案推进到可审计证明链条。
阅读原文