AI 生成并 Lean 形式验证 q 元 Hamming 立方体二次布尔函数的精确 junta 上界

YURAN XIU 在 Hexagon 首发论文，声称任意 q≥2 的 q 元 Hamming 立方体上次数至多 2 的布尔函数最多依赖 max{4,q+1} 个变量，并给出超过四变量时必存在 selector coordinate 的结构定理。作者说明两个结果均已用 Lean 4 / Mathlib 形式化且仅使用标准公理。页面披露主要 AI 生成、人类尚未理解全部证明；10 月 19 日另有 v2，10 月 17 日按首次公开 v1 收录。