Бернардо Суберкасо и Бенджамин Пшибоки опубликовали исследовательскую работу «A SAT Attack on Tarski’s High School Algebra Problem». В ней они объясняют задачу Тарского о выводимости тождеств со сложением, умножением и возведением в степень из 11 элементарных тождеств.

Работа опирается на результат Уилки. Указанное им тождество истинно для положительных целых чисел, но не выводится из аксиом Тарского.

С помощью SAT авторы доказали, что минимальный размер контрмодели равен 12, и подтвердили гипотезу Берриса и Йейтса. Они насчитали ровно 8 957 952 неизоморфные контрмодели на 12 элементах и предложили их простую классификацию.

По заявлению авторов, их SAT-подход превосходит Mace4 и SEM, специализированные инструменты поиска контрмоделей в эквациональных теориях. Корректность основного результата они также доказали в Lean с использованием автоформализации.

Проверка утверждений:

  • Бернардо Суберкасо и Бенджамин Пшибоки опубликовали исследовательскую работу «A SAT Attack on Tarski’s High School Algebra Problem», которая объясняет задачу Тарского о выводимости тождеств с сложением, умножением и возведением в степень из 11 элементарных тождеств. (подтверждено первоисточником: доказательство; «Title: A SAT Attack on Tarski’s High School Algebra Problem Authors: Bernardo Subercaseaux , Benjamin Przybocki View a PDF of the paper titled A SAT Attack on Tarski’s High School Algebra Problem, by Bernardo Subercaseaux and Benjamin Przybocki View PDF HTML (experimental) Abstract: 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:»)
  • До этой работы известные результаты дали контрмодель из 12 элементов, тогда как отдельно было доказано отсутствие контрмоделей размером менее 11 элементов. (подтверждено первоисточником: доказательство; «Gurevič gave an algebra on 59 elements that satisfies Tarski’s axioms but not Wilkie’s identity, and over the years several authors whittled down the size of such a countermodel, culminating in a countermodel of size 12 due to Burris and Yeats. On the other hand, Zhang proved that there is no countermodel with fewer than 11 elements.»)
  • С помощью SAT авторы доказали, что минимальный размер контрмодели равен 12, подтвердив гипотезу Берриса и Йейтса. (подтверждено первоисточником: доказательство; «Using SAT, we prove that the smallest countermodels are of size 12, as conjectured by Burris and Yeats.»)
  • Авторы насчитали ровно 8 957 952 неизоморфные контрмодели на 12 элементах и предложили их простую классификацию. (подтверждено первоисточником: доказательство; «Moreover, we show that there are exactly 8,957,952 countermodels on 12 elements up to isomorphism and provide a simple classification of them.»)
  • По заявлению авторов, их SAT-подход превосходит специализированные инструменты поиска контрмоделей в эквациональных теориях Mace4 и SEM. (подтверждено первоисточником: доказательство; «Our SAT approach outperforms dedicated tools for finding countermodels in equational theories, namely Mace4 and SEM.»)
  • Корректность основного результата авторы также доказали в Lean с использованием автоформализации. (подтверждено первоисточником: доказательство; «Furthermore, using autoformalization, we prove the correctness of our main result in Lean.»)

Первоисточники:

оценка 63.5 · тип research · ревизия 1 · истории st-pg8dez