公开项目提供一篇未署名数学论文、基于 mathlib Liouville 函数的完整 Lean 4 形式化、固定工具链元数据、构建与公理审计以及证明路线检查。另一个独立审计仓库 在 Linux 上重新构建冻结的 v1.0.0 产物，对照源码哈希并重复公理与路线审计， 报告未发现 sorry、自定义定理公理或 native_decide。
Captain Sude 公开将一项无条件证明归因于 GPT-6 Astra：对每个大于 2 的偶数 N， 都存在正整数 a、b，使 N = a + b 且 lambda(a) = lambda(b) = -1。公开论文与 Lean 定理均陈述这一覆盖全部偶数的结论，不依赖 GRH，也没有“充分大”限制。 这是二元哥德巴赫问题的 Liouville 类比，并非经典哥德巴赫猜想的证明。
公开项目提供一篇未署名数学论文、基于 mathlib Liouville 函数的完整 Lean 4 形式化、固定工具链元数据、构建与公理审计以及证明路线检查。另一个独立审计仓库 在 Linux 上重新构建冻结的 v1.0.0 产物，对照源码哈希并重复公理与路线审计， 报告未发现 sorry、自定义定理公理或 native_decide。由于公开论文和仓库没有保存 详细的模型—人类推导轨迹，Chronicle 对具体智力分工只做来源归因，不作独立重建。
Mangerel 2024 年关于 Shusterman 问题的论文，只在 GRH 假设下并对充分大的偶数 N 得到相同的 (-1,-1) 符号模式结论。此次发布声称同时去掉这两个限制，并把论证 封装为可复现的形式化产物。如果其数学新颖性与 Astra 来源归因继续经受专业审查， 该事件将体现 AI 参与解决具体开放研究问题，而不是仅仅提升基准成绩。
重要性说明：该成果针对一个已有明确记录的 Liouville–Goldbach 开放问题，给出覆盖全部偶数的 无条件定理，而最直接的前驱结果仍依赖 GRH 且只适用于充分大的偶数。公开成果同时 提供完整 Lean 形式化，并已有独立技术重放，因此足以构成实质性的 AI 参与研究里程碑； 但它不同于经典二元哥德巴赫猜想，且目前尚不足以达到 Chronicle 的 H1 历史级门槛。
公开仓库发布数学论文与完整 Lean 形式化，最终定理与所述覆盖全部偶数的 Liouville–Goldbach 主张一致；项目同时记录了成功的本地构建、公理审计和 证明路线审计。
一个独立审计仓库报告对冻结的 v1.0.0 版本完成 Linux 重建，源码哈希零差异， 重新执行公理审计和证明路线审计，并未发现 sorry、自定义定理公理或 native_decide。 这些证据支持 independently_replayed 的形式保障，但该审计明确属于技术复现， 并非独立数学同行评议或历史优先权裁决。
当前没有记录的更正。
