发表机构
Carnegie Mellon University（卡内基梅隆大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文通过SAT方法结合自动形式化在Lean中证明塔斯基高中代数问题的最小反模型规模为12，12元反模型共8957952个，且该方法优于Mace4、SEM等工具。
AI 中文摘要
塔斯基高中代数问题询问：所有关于正整数的加法、乘法和指数运算的恒等式是否都能由11条基本恒等式推导得出。令人惊讶的是，Wilkie证明了以下恒等式在正整数上成立，但无法从塔斯基公理推导得出：\begin{align*} &\left((1+x)^y + (1+x+x^2)^y\right)^x \cdot \left((1+x^3)^x + (1+x^2+x^4)^x\right)^y = \\\\ &\left((1+x)^x + (1+x+x^2)^x\right)^y \cdot \left((1+x^3)^y + (1+x^2+x^4)^y\right)^x. \end{align*}Gurevič给出了一个满足塔斯基公理但不满足Wilkie恒等式的59元代数，多年来多位学者逐步减小这类反模型的规模，最终Burris和Yeats得到了一个规模为12的反模型；另一方面，Zhang证明不存在规模小于11的反模型。本文利用SAT（可满足性问题）证明，最小的反模型规模确实为12，符合Burris和Yeats的猜想；还证明在同构意义下，12元反模型共有8957952个，并给出了简单分类。本文的SAT方法在寻找等式理论反模型的专用工具Mace4和SEM的对比中表现更优，此外，本文通过自动形式化在Lean中证明了主要结果的正确性。
英文摘要
Tarski's high school algebra problem asks whether every true identity concerning addition, multiplication, and exponentiation of positive integers follows from a list of 11 elementary identities. Surprisingly, Wilkie showed that the following identity is valid over the positive integers and yet does not follow from Tarski's axioms: \begin{align*} &\left((1+x)^y + (1+x+x^2)^y\right)^x \cdot \left((1+x^3)^x + (1+x^2+x^4)^x\right)^y = \\ &\left((1+x)^x + (1+x+x^2)^x\right)^y \cdot \left((1+x^3)^y + (1+x^2+x^4)^y\right)^x. \end{align*} Gurevič gave an algebra on 59 elements that satisfies Tarski's axioms but not Wilkie's identity, and over the years several authors whittled down the size of such a countermodel, culminating in a countermodel of size 12 due to Burris and Yeats. On the other hand, Zhang proved that there is no countermodel with fewer than 11 elements. Using SAT, we prove that the smallest countermodels are of size 12, as conjectured by Burris and Yeats. Moreover, we show that there are exactly 8,957,952 countermodels on 12 elements up to isomorphism and provide a simple classification of them. Our SAT approach outperforms dedicated tools for finding countermodels in equational theories, namely Mace4 and SEM. Furthermore, using autoformalization, we prove the correctness of our main result in Lean.
Comments21 pages. Accepted to LPAR 2026, v2 acknowledges arXiv:2608.16406 and fixes minor typos
