A SAT Attack on Tarski's High School Algebra Problem

论文把 Wilkie 恒等式的有限反模型搜索编码为 SAT，证明最小反模型恰为 12 元，而不是停留在已有的“至少 11 元”下界。在 12 元规模上，它按同构枚举出 8,957,952 个反模型并给出分类，还把自动形式化接到 Lean；SAT 枚举、结构归纳和形式验证的串联，是这项结果可复核的关键。