AI 辅助 Arad–Herzog 有限单群猜想证明主张公开：Lean 只完成依赖数百外部公理的条件性推导

Aran S. Ziegler 于 2026 年 10 月 19 日在 Zenodo 公开《Proof of the Arad–Herzog conjecture》的版本 3，声称完成 1985 年提出的有限非阿贝尔单群共轭类乘积猜想：两个非单位元共轭类的乘积至少包含两个共轭类。论文汇集已发表的交错群、特征标与有限 Lie 型群结果，并声称处理剩余情形及刻画奇维正交群中的特殊二类乘积。项目声明使用 OpenAI 与 Anthropic 的 agentic AI 工具推进研究策略、Lean 形式化与文稿。**这不是经过独立确认的猜想解决**：作者描述的 Lean 顶层结论是相对于大量文献分类与特征标假设的推导，依赖闭包含约 859 个公理/外部输入（其中约 269 项为具名非平凡数学假设），完整复核工件未公开；截至发布时没有独立专家审核。Zenodo 显示公开日期为 10 月 19 日，记录的更早技术创建时间不视为首次公开发表。