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 considered the following eleven axioms about addition ('+'), multiplication ('·'), and exponentiation to be standard axioms taught in high school:

These eleven axioms, sometimes called the high school identities, are related to the axioms of an exponential ring. Tarski's problem then becomes: are there identities involving only addition, multiplication, and exponentiation, that are true for all positive integers, but that cannot be proved using only the axioms 1–11?

Since the axioms seem to list all the basic facts about the operations in question it is not immediately obvious that there should be anything one can state using only the three operations that is not provably true. However, proving seemingly innocuous statements can require long proofs using only the above eleven axioms. Consider the following proof that (x + 1)² = x² + 2 · x + 1:

Here brackets are omitted when axiom 2. tells us that there is no confusion about grouping.

The length of proofs is not an issue; proofs of similar identities to that above for things like (x + y)¹⁰⁰ would take a lot of lines, but would really involve little more than the above proof.

The list of eleven axioms can be found explicitly written down in the works of Richard Dedekind, although they were obviously known and used by mathematicians long before then. Dedekind was the first, though, who seemed to be asking if these axioms were somehow sufficient to tell us everything we could want to know about the integers. The question was put on a firm footing as a problem in logic and model theory sometime in the 1960s by Alfred Tarski, and by the 1980s it had become known as Tarski's high school algebra problem.

...
Wikipedia