非sofic群问题牵动着sofic熵理论、动力系统遍历论和算子代数一整片数学版图。1999年阿贝尔奖得主Mikhail Gromov提出sofic群概念，核心问题极简洁：所有可数群都能用有限置换去逼近它的局部乘法表吗？27年间无数顶尖数学家尝试构造反例，全部折戟。Astra从数学工具箱里直接拎出二元Leavitt代数的单位群，结合Kun-Thom扩展图理论与汤普森群V的矛盾推导，首次构造出无限有限呈现的非sofic群，否定「所有可数群都是sofic」的猜想。

OpenAI发布Astra成果后不到两周，16位顶尖数学家联合发布长达11页的《莱顿宣言》，签名人数已达3164人，获国际数学联盟背书。宣言核心指出：数学不是单纯追求标准答案的工具，AI可批量生成大量低质量论文，极大加重同行评审负担，真正原创成果易被海量无效信息淹没。菲尔兹奖得主Timothy Gowers没有签署宣言，因为他认为AI带来的挑战更深远——不是数学会因停滞而死，而是会因证明过剩而亡。

Astra攻克了10个悬而未决数十年的难题，但OpenAI核心研究员Noam Brown坦言，目前尚未成功解决类似黎曼猜想这样的千禧年大奖难题。当下能看到的关键变量是：AI做数学的方式已从「解有答案的竞赛题」跃迁到「自主构造反例以推翻猜想」，且所有证明通过Lean 4形式化验证。拐点不在AI能否解出更难的问题，而在于数学界能否消化「证明过剩」时代的到来——陶哲轩警告，AI生成的证明堆在那里无人消化，审稿人「看不过来」已成常态。