Lean 4 形式化出 block sensitivity 与 spectral sensitivity 的 2.12+ 分离

RexDouglass · x · 2026-07-28

帖子称，关于 block sensitivity 与 spectral sensitivity 关系的结果已经在 Lean 4 中形式化完成，目前可证明二者之间至少存在 2.12 的指数差异；正文还提到正式写作仍在编辑中。

被引用内容进一步说明，gpt-5.6-sol 帮助推翻了“bs(f)=O(λ(f)^2)”的猜想：它找到了一个定义在 2^69 个输入上的函数，表明 block sensitivity 和 spectral sensitivity 不能用常数因子等价。核心看点是：一个复杂性理论结果被 Lean 形式化，而且 AI 参与了反例发现。