How SAT Solvers Cracked Tarski’s High-School Algebra

The algebra identity that shouldn’t be provable

Picture a worksheet equation that looks, at first glance, like it belongs to high-school algebra. It mixes only the operations you learned early: addition, multiplication, and exponentiation.

Now imagine a different question entirely. Not “Is the equation true?” but “Can it be derived from a short list of basic algebra rules?” That is the spirit of Tarski’s high school algebra problem: start with 11 elementary identities (often called the high school axioms) governing positive integers under addition, multiplication, and exponentiation, and ask whether every true identity must follow from those axioms. (en.wikipedia.org)

The surprising twist is that there exists a specific identity, commonly attributed to Wilkie, that really is true for all positive integers… yet cannot be proven from Tarski’s 11 axioms. The arXiv paper behind this post uses SAT solving—a workhorse technique from theoretical computer science—to show the smallest possible “countermodels” where the axioms hold but Wilkie’s identity fails. (arxiv.org)

From “true over integers” to “countermodel”

To understand what a countermodel means, it helps to unpack some logic vocabulary.

• A model (in logic) is a concrete mathematical universe where all axioms are interpreted as true.
• A countermodel is a model where the axioms hold, but a particular claim (like Wilkie’s identity) does not.
• Two models are considered the same up to isomorphism if there is a relabeling of elements that turns one model into the other.

So the counterexample goal becomes: build a finite structure with a finite set of elements, define operations that mimic addition, multiplication, and exponentiation, make all 11 axioms true inside that structure, and then arrange things so Wilkie’s identity fails.

This is where the problem feels like it changes genres. Algebra becomes model-building; identities become constraints; proof becomes search. (math.ucr.edu)

Why the number “12” mattered so much

Over the years, researchers repeatedly improved upper bounds by finding smaller countermodels. The history reads a bit like a videogame speedrun: start with a large “working-but-not-optimized” countermodel, then shave it down.

The arXiv abstract sketches the arc: Gurevič produced a countermodel of size 59, later work reduced the size step by step, and Burris and Yeats reached size 12 while conjecturing that this would be optimal. ()

Then Zhang proved a lower bound: there is no countermodel with fewer than 11 elements. That result pins the question down sharply. If nothing smaller than 11 works, and size 12 is known to work, then the main uncertainty is whether 11 could work, or whether 12 really is the first size where things become possible. ()

The new paper confirms exactly what the conjecture suggested:

• The smallest countermodels have size 12.
• Up to isomorphism, there are exactly 8,957,952 such countermodels.
• The authors provide a classification of these 12-element countermodels.

That’s the core mathematical result, and it’s the motivation for the technical part: how to find and verify an enormous combinatorial object count reliably. ()

What SAT solving is (and why it fits this problem)

SAT stands for Boolean satisfiability: a SAT solver is a program that answers whether a given formula in logic—built from variables that are either true or false—can be made true.

A formula in SAT is typically written as a collection of clauses, where each clause is an OR of some variables (or their negations). The solver searches for an assignment of truth values that satisfies all clauses at once.

The key trick in the paper is conceptually simple even if the implementation is not: turn “find a countermodel” into “find a truth assignment that satisfies constraints.” Once the constraints are in SAT form, you can harness the performance of modern SAT engines.

The reason this is a good match for equational logic is that finite algebra structures translate cleanly into finite constraint systems:

1. Choose a finite set of size n.
2. Represent each operation (addition, multiplication, exponentiation) by tables: for each pair (a, b), store the resulting element.
3. Encode the 11 axioms as logical constraints on those tables.
4. Encode “Wilkie’s identity fails” as an additional constraint that becomes false in the intended interpretation.

When n = 12, the search space is huge—but the structure of the constraints can still be navigated effectively by SAT. ()

Why Mace4 and SEM weren’t enough

The paper compares its approach to classic finite model finders designed for algebraic and first-order reasoning.

Two named tools show up:

• Mace4: a program for searching finite countermodels and models for first-order and equational statements. It works by constructing candidate structures for increasing domain sizes, and it can reduce parts of the problem to propositional reasoning. (mcs.anl.gov)
• SEM: another finite model generator whose search strategy includes symmetry-breaking techniques intended to cut away isomorphic or equivalent partial candidates. (lcs.ios.ac.cn)

Those tools can absolutely succeed—but the arXiv result claims the SAT-based method outperforms them for this particular equational theory. The deeper lesson is that equational countermodel hunting often has a “sweet spot” where SAT encodings scale better than backtracking model construction.

If you’ve ever felt like a search algorithm “wastes time being clever in the wrong direction,” this is the same story: the authors’ encoding makes the solver’s job align with the math’s structure. ()

Classification: counting models without getting lost

Finding one countermodel is enough to show that Wilkie’s identity doesn’t follow from Tarski’s axioms. But this paper goes far beyond existence.

Counting “8,957,952 up to isomorphism” means the authors aren’t just stumbling into solutions. They also handle equivalence under relabeling, which is crucial; otherwise the raw number of solutions explodes by a factor related to permutations of the underlying set.

To make that manageable, a practical pipeline usually combines:

• A SAT search to generate candidates,
• symmetry handling to avoid overcounting equivalent structures,
• and explicit verification that the axioms truly hold while Wilkie’s identity fails.

This is where the “attack” framing makes sense: the solver doesn’t attack integers directly. It attacks the constraint space of operation tables, and the result is a fully characterized family of 12-element countermodels. ()

Lean autoformalization: proving the SAT result, not just trusting it

SAT solvers are fast, but they are not magic. A solver returning “satisfiable” doesn’t automatically mean the mathematics is sound unless the translation from algebra to SAT and back is correct.

The paper reports that the main result is proven in the Lean theorem prover using autoformalization. Lean is a proof assistant: it checks proofs by verifying logical steps in a formal system.

Autoformalization is the umbrella term for tooling that translates a mathematical claim into machine-checkable Lean code, often with help from automation pipelines. In this context, the authors are using Lean to certify that their SAT-based counting and classification results correspond to genuine countermodels satisfying the intended axioms and violating Wilkie’s identity.

That matters because it closes the loop:

• SAT finds candidates efficiently,
• the encoding is validated by logical correctness,
• and Lean provides a final, checkable proof that the “smallest countermodels have size 12” statement really follows.

It’s a nice reminder that modern math tooling often works best as a team: SAT for search, proof assistants for trust. ()

The bigger story: why this feels like a collision of worlds

At first, the phrase “SAT attack” sounds dramatic, like cryptography. But here it’s more like engineering.

Tarski’s high school algebra problem sits at the boundary of:

• mathematical logic (axioms, derivability, countermodels),
• algebra (finite structures with operations), and
• computational logic (SAT encodings, symmetry handling, automated verification).

The identity itself is “high school algebra” style, but the modern question is about what can or cannot be forced by axioms inside a logical system. The surprising punchline is that the smallest counterexample size lands exactly where human conjectures predicted—then gets pinned down with a full classification obtained by SAT and certified with Lean. ()

Closing thought

Why does a Boolean satisfiability solver end up at the center of a question about exponentiation identities? Because the moment the problem is rephrased as “build operation tables satisfying constraints,” the algebra becomes a giant system of yes/no decisions.

And once that transformation happens, the machine can do what it’s built for: search vast combinatorial spaces efficiently, then hand the result back to logic so it can be trusted.

That’s the real discovery here—not only that 12 is the smallest countermodel size, but that a carefully designed computational pipeline can turn a subtle logical separation into something you can classify, count, and formally verify.