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.
Using SAT, we prove that the smallest countermodels are of size 12, as conjectured by Burris and Yeats.
- zero_k
Markus Anders, who wrote the symmetry breaking system (satsuma) they use for SAT is pretty much a genius. His version of Kissat won the SAT Competition this year, with satsuma of course:
https://satcompetition.github.io/2026/downloads/satcomp26sli...
See slide 18. It was really nice to see him win. I have always been a huge fan of symmetry breaking, CryptoMiniSat (that I develop) had a symmetry breaking system, BreakID (which is _way_ slower than Markus' satsuma), in it for many years now.
- NooneAtAll3
I love SAT solver papers, always interesting to see auxiliary variable techniques, since those aren't really listed anywhere central
here for example, instead of saying {f(x,y,z)==g(x,y,z)}, authors instead make variable group a_w:=(f(x,y,z)=w||g(x,y,z)=w), and then apply "at most 1" to it. Can't be unequal if both functions only can have 1 result in total
this adds an index to iterate over, but separates internal subexpressions of f() and g(), removing 2 indixes (in this problem) and thus dropping whole power of n of clauses
---
what I don't get is that they aren't searching Tarski's problem per se, but for one specific solution to it (one identity that isn't resulting from given). I'd totally look for arithmetic models that violate expectations in other ways than Wilkie
- 406380581
The lower bound had already been established in prior work: https://zenodo.org/records/18568303
- munchler
Why is subtraction not part of the algebra? It’s certainly familiar to every high school math student. This omission allows the counterexample, so the reveal is a bit of a disappointment IMHO.
- LPisGood
They address the following concern of Zhang (2005), which contained prior work involving similar techniques:
> […] Of course, this conclusion is not proved mathematically. It is possible that the programs have some bugs, or the user (myself made some errors.
They address it as follows:
> We address this [… through] ChatGPT 5.5 Pro, through Codex, to automatically generate a Lean formalization that we then checked ourselves to confirm the statements and definitions indeed match their expected semantics. This process took multiple iterations and discussions with the model over several days, and generated over 10,000 lines of code.
This is extremely unconvincing. Manual review of 10,000 lines of AI generated code is a terrifying prospect. I’m sure the result is correct, however I am deeply uncomfortable with this being mankind’s new mathematical process. Similar concerns have been expressed since the days of the 4 color theorem, but this feels different. Perhaps it is just new.
>in a nutshell, it defines an executable function encode that takes a natural number n ≥ 5 and emits a CNF formula, which is byte-for-byte equal to the output of our Python encoding
The phrase “byte-for-byte equal” makes my eye twitch these days.