Claude 辅助解决 Welch 函数三阶 sum-free 猜想，Kloosterman 和 + 有限域证书明确核验边界

Deep Bhattacharjee 于 10 月 22 日报告证明 Hou–Zhao 关于 Welch 幂函数 X^(2^m+3) 在 F_(2^n)、奇数 n≥7 情况下不是 third-order sum-free 的猜想：利用 binary Kloosterman sum K_n 给出允许零和三维仿射子空间的精确计数 (2^n+1−3K_n)/4，并用 Weil 界推出正性。Claude Code 完成辅助检索、推导与多语言验证程序；Lean 4 仅形式化若干代数恒等式及 n=5,7 的有限证书，**未声称所有 n 的分析论证都被 Lean end-to-end 核验**。