Captain Sude 将 Liouville–Goldbach 问题的无条件证明归因于 GPT-6 Astra，并公开完整 Lean 4 形式化

公开项目证明：每个大于 2 的偶数 N 都可写成 N=a+b，其中 a、b 的 Liouville 函数值都为 -1。仓库给出论文、最终 Lean theorem、固定 Lean/mathlib 版本，以及 build、axiom 和 proof-route audit；另有独立 Linux replay。该结论是经典二元 Goldbach 的 Liouville 类比，并不是经典 Goldbach 猜想本身。