Tarski's high school algebra problem

In mathematical logic, Tarski's high school algebra problem was a question posed by Alfred Tarski. It asks whether there are identities involving addition, multiplication, and exponentiation over the positive integers that cannot be proved using eleven axioms about these operations that are taught in high-school-level mathematics. The question was solved in 1980 by Alex Wilkie, who showed that such unprovable identities do exist.

Tarski's problem more formally asks if the equational theory of the High School Axioms ${\displaystyle {\text{Th}}_{Eq}(\mathrm {HS} )}$ (that is, the set of identities provable from them in equational logic) is equal to the equational theory of ${\displaystyle \mathbb {R} _{\geq 0}}$ (that is, the set of all true identities)?

This turns out to be analogous to Hilbert's program and Gödel's incompleteness theorem in the 1920s and 30s. First, note that Birkhoff proved with his HSP theorem that, remarkably, the equational theory of ${\displaystyle \mathbb {R} _{\geq 0}}$ is equal to the equational theory of all commutative semirings, in particular the equational theory of ${\displaystyle \mathbb {N} }$. In other words, to test if an identity is true one only needs to test it for natural numbers.

Then, one can ask if the first-order theory of some finite set of axioms (that is, the set of formulas provable from them in first-order logic) is equal to the first-order theory of the natural numbers, ${\displaystyle {\text{Th}}(\mathbb {N} )}$ (that is, the set of all true formulas). In Tarski's question the goal is for ${\displaystyle {\text{Th}}_{Eq}(\mathrm {HS} )={\text{Th}}_{Eq}(\mathbb {N} )}$; in Hilbert's question the goal is for a theory ${\displaystyle T}$ for which ${\displaystyle {\text{Th}}(T)={\text{Th}}(\mathbb {N} )}$.

In both cases this does not work out. Godel's first incompleteness theorem, which shows that ${\displaystyle {\text{Th}}(\mathbb {N} )}$ is not computably axiomatizable, is then analogous to Wilkie and Gurevič's results that the equational theory is not finitely axiomatizable.