How SAT Solvers Cracked Tarski’s High-School Algebra
Tarski’s high school algebra problem asks whether every true integer identity follows from 11 basic axioms. Using SAT solving and Lean verification, a new result shows the smallest countermodels have size 12 and there are exactly 8,957,952 of them up to isomorphism.