Summary (Overview)

• Main result: The paper confirms the Burris-Yeats conjecture that the smallest countermodels to Wilkie's identity (an identity valid over positive integers but not derivable from Tarski's high school axioms) have exactly 12 elements.
• Enumeration: The authors prove there are exactly $2^{12} \cdot 3^7 = 8{,}957{,}952$ countermodels of size 12 up to isomorphism, providing a complete classification via a template with independent parameters.
• SAT approach outperforms dedicated tools: The lower bound (no countermodels of size ≤ 11) is established in ~10 minutes, while a 12-element countermodel is found in ~50 minutes—dramatically faster than prior approaches using Mace4 and SEM which required weeks/months.
• Formal verification: The authors use autoformalization with ChatGPT 5.5 Pro to generate a Lean formalization, proving the correctness of their main result with a verified LRAT certificate.
• Key techniques: The success relies on symmetry-breaking constraints (lex-leader), auxiliary variables to reduce encoding size, and problem-specific lemmas from prior literature.

Introduction and Theoretical Foundation

Tarski's High School Algebra Problem asks whether every true identity about addition, multiplication, and exponentiation of positive integers follows from 11 elementary axioms:

$$x + y = y + x \quad \text{(HSI 1)}$$ $$(x + y) + z = x + (y + z) \quad \text{(HSI 2)}$$ $$x \cdot 1 = x \quad \text{(HSI 3)}$$ $$x \cdot y = y \cdot x \quad \text{(HSI 4)}$$ $$(x \cdot y) \cdot z = x \cdot (y \cdot z) \quad \text{(HSI 5)}$$ $$x \cdot (y + z) = x \cdot y + x \cdot z \quad \text{(HSI 6)}$$ $$1^x = 1 \quad \text{(HSI 7)}$$ $$x^1 = x \quad \text{(HSI 8)}$$ $$x^{y+z} = x^y \cdot x^z \quad \text{(HSI 9)}$$ $$(x \cdot y)^z = x^z \cdot y^z \quad \text{(HSI 10)}$$ $$(x^y)^z = x^{y \cdot z} \quad \text{(HSI 11)}$$

Wilkie's Identity (1981) is valid over $(\mathbb{Z}_{>0}, +, \cdot, \uparrow, 1)$ but does NOT follow from HSI axioms:

$$\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 identity holds because $1 + x^3 = (1+x)(1-x+x^2)$ and $1+x^2+x^4 = (1+x+x^2)(1-x+x^2)$, but subtraction is not in the language, so this reasoning cannot be carried out within the axiomatic system.

Historical bounds: Gurevič (1985) found the first countermodel of size 59; Burris and Yeats (2004) reduced the upper bound to 12; Zhang (2005) proved a lower bound of 11. These bounds are summarized in Table 1.

Methodology

SAT Encoding of HSI Algebras

The authors encode the existence of an HSI algebra of size $n$ as a CNF formula. Elements are identified with $D_n = \{\bar{1}, \bar{2}, \ldots, \bar{n}\}$, with variables:

• $\mathsf{A}_{i,j,k}$: $\bar{i} + \bar{j} = \bar{k}$ (only for $i \leq j$ due to commutativity)
• $\mathsf{M}_{i,j,k}$: $\bar{i} \cdot \bar{j} = \bar{k}$ (only for $i \leq j$)
• $\mathsf{E}_{i,j,k}$: $\bar{i}^{\bar{j}} = \bar{k}$ (all $i,j,k$)

Functionality constraints (each operation must yield exactly one result):

$$\forall i \in [n], \forall j \in \{i,\ldots,n\}, \quad \sum_{k \in [n]} \mathsf{A}_{i,j,k} = 1$$

Key optimization: Instead of the naïve $O(n^6)$ encoding for associativity (HSI 2), the authors introduce auxiliary variables $\mathsf{A}^2_{i,j,k,\ell}$ representing whether $(\bar{i}+\bar{j})+\bar{k} = \bar{\ell}$ or $\bar{i}+(\bar{j}+\bar{k}) = \bar{\ell}$, reducing to $O(n^5)$ clauses.

Encoding Wilkie's Identity Negation

The authors fix the failing pair to be $(\bar{4}, \bar{5})$ without loss of generality (justified by Lemma 4.1 ensuring 1, a, b, 1+1, 1+1+1 are all distinct). They build variables for each subexpression of LHS and RHS, culminating in:

$$\bigwedge_{v=1}^{n} (\neg \mathrm{LHS}_v \vee \neg \mathrm{RHS}_v)$$

Additional Constraints

Key lemmas incorporated to speed up search:

• Lemma 4.1: Elements $\bar{1}, \bar{a}, \bar{b}, \bar{1}+\bar{1}, \bar{1}+\bar{1}+\bar{1}$ are all distinct
• Lemma 4.2: 16 inequalities (e.g., $\bar{1}+\bar{a} \neq \bar{1}$, $\bar{a}\cdot\bar{a} \neq \bar{1}$, etc.)
• Lemma 4.3: Non-divisibility conditions $P \nmid Q$, $Q \nmid P$, $R \nmid S$, $S \nmid R$ where $P = 1+a$, $Q = 1+a+a^2$, $R = 1+a^3$, $S = 1+a^2+a^4$
• Lemma 4.4: $\bar{b} \neq \bar{i} + \sum_{j=1}^{m} \bar{i_j} \cdot \bar{a}^j$ for integers $i, i_j$

Symmetry Breaking

Lex-leader constraints enforce that for each pair of indistinguishable elements $i, j$ with $6 \leq i < j \leq n$:

$$\vec{\mathsf{A}} \circ \vec{\mathsf{M}} \circ \vec{\mathsf{E}} \preceq_{\text{lex}} s_{i,j}(\vec{\mathsf{A}} \circ \vec{\mathsf{M}} \circ \vec{\mathsf{E}})$$

Empirical Validation / Results

Experimental Performance

The full formula $\Omega_n$ was solved with Kissat 4.0.4 on a MacBook Pro M5:

Without symmetry breaking, the formula $\Omega_n^{\text{no-sim}}$ performs significantly worse (e.g., n=10 takes 1,843.52s vs 65.84s), confirming the importance of lex-leader constraints.

Lean Verification

The authors generated a DRAT proof (368 MB, verified in 3,781s) and converted it to LRAT (2.2 GB, imported in 757s via LRAT-Catcher). They formalized the entire encoding in Lean, proving:

theorem no_generalCountermodel_of_order_le_eleven {n : Nat} (hn : n ≤ 11) :
¬ ∃ A, GeneralCountermodel n A

Classification of 12-Element Countermodels

The classification consists of:

• Addition table: 3 options for α-parameters × $2^8$ independent choices for β-parameters = 768 possibilities
• Multiplication table: Fixed, no free parameters
• Exponentiation table: 3 options for γ-parameters × $3^5$ choices for δ-parameters × 16 choices for ε-parameters = 11,664 possibilities

Total: $768 \times 11{,}664 = 8{,}957{,}952$ models, all non-isomorphic.

Theoretical and Practical Implications

1. Resolution of the Burris-Yeats conjecture: The smallest countermodels to Wilkie's identity have exactly 12 elements, confirming the conjecture from 2004.

2. Methodological contributions: The paper demonstrates that modern SAT solvers with proper symmetry breaking and encoding optimizations dramatically outperform dedicated finite model finders (Mace4, SEM) for this class of problems. Zhang's claim that "SAT-based tools are not so advantageous" is directly refuted.

3. Formal verification pipeline: The paper showcases a workflow combining autoformalization (via ChatGPT), SAT solving, and interactive theorem proving (Lean) to produce fully verified mathematical results—addressing concerns about the trustworthiness of computational proofs.

4. New mathematical insights: The classification enables deriving new results, e.g., showing there are exactly $8{,}957{,}952/3 = 2{,}985{,}984$ countermodels to a univariate identity obtained by substituting $y = 3^x$, and confirming Gurevič's conjecture about the minimality of the identity with $y = 2^x$ by finding a 13-element countermodel.

Conclusion

The paper establishes that the smallest HSI algebras in which Wilkie's identity fails have exactly 12 elements, confirming the Burris-Yeats conjecture, and provides a complete classification of the $8{,}957{,}952$ such algebras up to isomorphism. The SAT-based approach, enhanced with lex-leader symmetry breaking and auxiliary variables, outperforms dedicated finite model finders by orders of magnitude, and the results are formally verified in Lean.

Open questions:

• Question 1: What is the smallest $n$ for which there exists an HSI algebra of order $n$ that does not satisfy ALL identities valid over $(\mathbb{Z}_{>0}, +, \cdot, \uparrow, 1)$? The best published lower bound is 3 (Asa04), with 12 as the current upper bound.
• The authors suggest their techniques could be applied to other algebraic problems, such as the equational theories project's open implication question about magmas.