Analysis of "A SAT Attack on Tarski's High School Algebra Problem"

Authors: Bernardo Subercaseaux & Benjamin Przybocki
Reference: arXiv:2608.08421 | Date: August 9, 2026
Field: Logic (math.LO) and Logic in Computer Science (cs.LO)

---

📌 Overview of the Problem

The central focus of this research is Tarski's High School Algebra Problem. This mathematical inquiry asks a fundamental question: Can every identity involving the addition, multiplication, and exponentiation of positive integers be derived from a specific set of 11 elementary axioms?

While it seems intuitive that these basic rules should cover all truths, the answer is no.

The Wilkie Discovery: A mathematician named Wilkie identified a specific identity that is mathematically valid for all positive integers but cannot be proven using Tarski's 11 axioms.

The Wilkie Identity

The identity in question is expressed as:

$\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$

---

🔍 The Quest for Countermodels

To prove that an identity does not follow from a set of axioms, researchers look for countermodels—algebraic structures that satisfy the axioms but fail to satisfy the identity.

Evolution of Countermodel Sizes

The search for the smallest possible countermodel has been a gradual process of refinement:

---

🛠️ Methodology: The SAT Attack

The authors utilized SAT (Satisfiability) solvers to resolve the conjecture regarding the minimum model size. Their workflow can be visualized as follows:

Key Technical Achievements

• Performance: The SAT-based strategy was found to be more efficient than traditional dedicated equational theory tools such as Mace4 and SEM.
• Verification: To ensure the results were mathematically rigorous, the authors employed autoformalization to verify the findings within the Lean theorem prover.

---

📈 Results and Findings

The study yielded several definitive conclusions regarding the nature of these countermodels:

• Minimum Size: Confirmed that the smallest countermodels consist of exactly 12 elements.
• Enumeration: Identified exactly 8,957,952 distinct countermodels of size 12 (up to isomorphism).
• Classification: Provided a streamlined classification system for these millions of models.

Implementation Note

The authors' approach can be summarized by the following logic:

def verify_tarski_conjecture():
    for size in range(1, 12):
        if sat_solver.check(axioms, not_wilkie, size):
            return "Countermodel found smaller than 12"
    return "Minimum size is 12"

---

📄 Document Metadata

• Length: 21 pages.
• DOI: 10.48550/arXiv.2608.08421
• Submission History: v1 submitted on Sunday, August 9, 2026.

Image: The research was hosted on arXiv, a repository for scientific preprints.