A SAT Attack on Tarski's High School Algebra Problem

What grabbed attention was not the math claim itself so much as the machinery. People who know SAT focused on the encoding tricks, especially auxiliary-variable constructions that cut clause growth and the heavy use of symmetry breaking through satsuma and Kissat. The paper’s real signal is that careful encoding beat brute force. One author gave a concrete example: their size-10 lower-bound instance takes about 50k variables and 2.7M clauses and solves in about 85 seconds with Kissat, while a previously unnoticed Zenodo artifact used a different encoding with far fewer variables but 33M clauses and took about 50 minutes. That sharpened the practical lesson that clause structure and ordering matter more than headline variable counts. A second thread was about trust. The paper says ChatGPT 5.5 Pro and Codex helped produce more than 10,000 lines of Lean, intended to emit CNF formulas byte-for-byte identical to the Python encoder. Some readers found that alarming. The pushback was that in this case the formalized statements are narrow and easy to inspect, and exact output equality matters because SAT performance is sensitive to variable and clause ordering. Even so, people pointed out that proof assistants are not magical. A recent Lean soundness incident was cited as a reminder that typechecking reduces risk, but does not eliminate it. The bottom line was pragmatic: the paper looks like a serious SAT-engineering result with sensible formal checking, but the strongest confidence comes from the simplicity of what was formalized, not from “AI-generated Lean” as a category.