Claude 完成三元哥德巴赫猜想在 Lean 4 与 Mathlib 中的完整形式化

Claude 完成了三元哥德巴赫猜想在 Lean 4 与 Mathlib 中的形式化证明，所称主定理不含 sorry，仅依赖 Lean 标准三条公理。证明将 Platt 的 GRH 验证（q=1 时 RH 验证到 10^8）与二元哥德巴赫验证到 4×10^18 作为显式假设引入，回应了原始证明计算冗长、正确性难核对的问题。