SAT 공격으로 타르스키 고등학교 대수 문제의 최소 반례 12개 원소 증명

A SAT Attack on Tarski's High School Algebra Problem

Tarski의 고등학교 대수 문제는 양의 정수의 덧셈, 곱셈, 지수에 관한 모든 참인 항등식이 11개의 기본 공리에서 유도되는지 묻는다. Wilkie는 이 공리들로 증명할 수 없는 항등식을 발견했고, Gurevič는 59개 원소 반례를 제시했다. 이후 연구로 반례의 크기는 12까지 줄었고, Zhang은 11개 미만의 반례가 없음을 증명했다. 본 연구는 SAT를 사용해 최소 반례의 크기가 12임을 증명하고, 동형까지 정확히 8,957,952개의 반례가 존재함을 보이며 분류를 제공한다. SAT 접근법은 Mace4와 SEM 같은 전용 도구보다 뛰어났으며, autoformalization을 통해 Lean으로 결과의 정확성을 검증했다.