Smallest Countermodels for Tarski's High School Algebra Problem Found via SAT

A SAT Attack on Tarski's High School Algebra Problem

Tarski's high school algebra problem asks whether all true identities about positive integers' addition, multiplication, and exponentiation follow from 11 elementary axioms. Wilkie found a counterexample identity, and Gurevič provided a 59-element algebra. Over time, the countermodel size was reduced to 12. Using SAT, we prove that 12 is indeed the minimum, confirming a conjecture by Burris and Yeats. We also show there are exactly 8,957,952 countermodels of size 12 up to isomorphism and classify them. Our SAT approach outperforms dedicated tools like Mace4 and SEM, and we verify our main result in Lean.