Claude 搜索与 Lean 核验给出 book Ramsey 数 R(B57,B58)=231 的精确证书

Deep Bhattacharjee 于 10 月 22 日报告精确计算 book Ramsey number R(B_57,B_58)=231，构造 230 顶点二分块 circulant graph 使其不含 B57、补图不含 B58，结合已有 Rousseau–Sheehan 上界封闭该实例。Claude Code 产生构造、C/Python 独立检查以及 Lean 4 形式化；作者称纸面论证可化为 Z115 上 57 项不等式，核验程序枚举 26,335 个点对，Lean kernel 以 decide 而非 native_decide 校核目标。只证明该特定 Ramsey 数，并未解决 Wesley 一般猜想；本轮没有自行运行 Lean。