Бернардо Суберкасо и Бенджамин Пшибоцки атаковали задачу Тарского о школьной алгебре с помощью SAT. Работа называется A SAT Attack on Tarski's High School Algebra Problem и выложена на arXiv 9 августа 2026 года. Тарский спрашивал: выводится ли каждое истинное тождество про сложение, умножение и возведение в степень положительных целых из списка из 11 элементарных аксиом? Неожиданно выяснилось, что нет. Уилки предъявил тождество, которое верно для положительных целых, но не выводится из аксиом Тарского. Это означало, что аксиомы неполны. Само тождество — равенство двух длинных выражений, в котором используются только сложение, умножение и степени. Гуревич построил алгебру на 59 элементах, которая удовлетворяет аксиомам Тарского, но нарушает тождество Уилки. Позже несколько авторов уменьшали размер такой контрмодели, пока Беррис и Йитс не довели её до 12 элементов. Они же предположили, что 12 — это минимум. Чжан, с другой стороны, доказал, что контрмоделей с менее чем 11 элементами не бывает. Так к моменту работы были известны границы: нижняя 11, верхняя 12. Вопрос, существует ли контрмодель на 11 элементах, оставался открытым.
Авторы свели поиск контрмоделей к задачам SAT и доказали, что минимальная контрмодель имеет размер 12, как и предполагали Беррис и Йитс. Ни одна 11-элементная алгебра не подошла. То есть разрыв между границами закрыт. Итог: 12 элементов — точный минимум. Более того, с точностью до изоморфизма на 12 элементах таких контрмоделей ровно 8 957 952, и для них дана простая классификация. SAT-подход оказался быстрее специализированных инструментов поиска контрмоделей в теориях уравнений — Mace4 и SEM. Дополнительно корректность основного результата проверена в Lean: доказательство автоформализовано и успешно прошло проверку.