用 SAT 攻击 Tarski 中学代数问题：最小反例模型确为 12 个元素

概述

这篇数学论文用 SAT 求解器研究 Tarski 的中学代数问题——询问所有关于正整数加法、乘法、幂运算的真等式是否都能从 11 条初等恒等式推出。Wilkie 曾给出一个成立却不含于 Tarski 公理的恒等式，Gurevič 构造了满足公理但不满足 Wilkie 恒等式的 59 元代数，后来被逐步缩小到 12 个元素；Zhang 则证明不存在少于 11 个元素的反例。作者用 SAT 证明了最小反例模型恰为 12 个元素（印证 Burris-Yeats 猜想），且共有 8,957,952 个（同构意义下）12 元反例并给出分类，还借助自动形式化在 Lean 中证明了主结果的正确性。