AI 生成并声称经 Lean 验证的三多项式反例，否定有效超立方体 Nullstellensatz 的朴素推广

YURAN XIU 于 10 月 18 日发表理论计算机科学 / 代数组合学新反例：对每个 n≥1，用 2n+1 个变量构造次数分别为 2、2、1 的三个实多项式，乘积在布尔立方体上处处为零、无共同布尔零点，但任何相应 Nullstellensatz 证书的特定多线性化分量次数至少 n+1。构造从 Kothari 等此前关于两多项式的障碍出发，引入 selector variable 把高次数障碍转移至三多项式乘积零设置。论文声称整个无界次数反例已在 Lean 4 核验，Hexagon 标注 primarily AI-generated、human understanding no parts；外部未独立复核。