This paper resolves Tarski's high school algebra problem by proving that the smallest countermodels to Wilkie's identity have exactly 12 elements, confirming a conjecture by Burris and Yeats. The authors use SAT-based methods to enumerate and classify all 8,957,952 non-isomorphic countermodels on 12 elements, outperforming dedicated tools like Mace4 and SEM.
Background
Tarski's high school algebra problem (1930) asked whether all true identities about positive integers under +, *, ^ follow from 11 elementary axioms. Wilkie (1980) showed this is false by constructing a counterexample, but finding the smallest countermodel remained open for decades.
- Source
- Lobsters
- Published
- Aug 31, 2026 at 01:08 AM
- Score
- 8.0 / 10