Claude Fable 与 Codex 辅助给出离散四顶点定理的逆定理，并以 Lean / Palomar 验证几何存在性

Kristoffer Josefsson 于 10 月 17 日公开论文，回应 Tabachnikov 问题：对所有 n≥4，循环排列的正数只要至少有两个局部极大与两个局部极小，就可表示为满足特定圆心角条件的凸多边形相邻三点外接圆半径；并讨论局部 C¹ 连续选取与全局障碍。论文声称存在性和连续性部分已在 Lean 4 / Mathlib 形式化，并对应 Palomar 2026-10-17-000001；披露列出 Claude Fable、Codex 的参与且作者声明理解全部内容。