{"id":"arxiv/2608.08421","url":"https://arxiv.org/abs/2608.08421","tags":["math.LO","cs.LO"],"score":0,"title":"A SAT Attack on Tarski's High School Algebra Problem","domain":"math.LO","source":"arxiv","authors":["Bernardo Subercaseaux","Benjamin Przybocki"],"reviews":0,"subject":"math.LO","summary":"Tarski's high school algebra problem asks whether every true identity concerning addition, multiplication, and exponentiation of positive integers follows from a list of 11 elementary identities. Surprisingly, Wilkie showed that the following identity is valid over the positive integers and yet does not follow from Tarski's axioms: \\begin{align*} &\\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. \\end{align*} Gurevič gave an algebra on 59 elements that satisfies…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-09","reactions":{}}