SAT攻撃で「タルスキの高校代数問題」の最小反例モデルを解明

A SAT Attack on Tarski's High School Algebra Problem

タルスキの高校代数問題は、正の整数の加算・乗算・冪乗に関する真の等式が、11個の基本公理から導けるかどうかを問うものです。Wilkieは公理から導けない恒等式を発見し、Gurevičは59要素の反例モデルを構築しました。その後、BurrisとYeatsは12要素の反例モデルを発見し、Zhangは11要素未満の反例が存在しないことを示しました。本研究ではSATソルバーを用いて、最小の反例モデルが12要素であることを証明し、同型を除いて8,957,952個の反例モデルが存在することを示しました。さらに、自動形式化によりLeanで証明の正しさを検証しました。