A SAT Attack on Tarski's High School Algebra Problem
Abstract
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: &((1+x)y + (1+x+x2)y)x · ((1+x3)x + (1+x2+x4)x)y = &((1+x)x + (1+x+x2)x)y · ((1+x3)y + (1+x2+x4)y)x. 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.
Related
- A Van Hiele–Newman model analysis of geometric reasoning and problem-solving errors among final-year students in a selected senior high school
- An event is a set, not a number: building the algebra of events before the probability measure in a school progression
- Non-sofic Tarski monsters
- Inconclusive prospective effects between technology acceptance, classroom distraction, and academic engagement among Chinese high school students: A reassessment of Li and Chen (2026)
- Trends in mathematics achievement among Ghanaian senior high school students: an analysis of performance patterns and contributing factors
BibTeX
@misc{subercaseaux2026attack,
title = {{A SAT Attack on Tarski's High School Algebra Problem}},
author = {Bernardo Subercaseaux and Benjamin Przybocki},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2608.08421},
eprint = {2608.08421},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2608.08421},
}
RIS
TY - UNPB
TI - A SAT Attack on Tarski's High School Algebra Problem
AU - Bernardo Subercaseaux
AU - Benjamin Przybocki
PY - 2026
DA - 2026/09/02
PB - arXiv
DO - 10.48550/arxiv.2608.08421
UR - https://arxiv.org/abs/2608.08421
AB - 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: &((1+x)^y + (1+x+x^2)^y)^x · ((1+x^3)^x + (1+x^2+x^4)^x)^y = &((1+x)^x + (1+x+x^2)^x)^y · ((1+x^3)^y + (1+x^2+x^4)^y)^x. 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.
ER -