빈 육각형 수의 형식 검증

최근 컴퓨터 보조 수학의 획기적인 발전은 일반 위치에 있는 평면의 30점 집합(즉, 공통 직선 위에 세 점이 없는 경우)이 빈 볼록 육각형을 포함한다는 것을 보여 주었으며, 이는 1930년대로 거슬러 올라가는 연구 분야를 마무리 짓는 결과입니다. 기하학적 통찰력과 자동화된 추론 기법의 조합을 통해 Heule과 Scheucher는 O(n⁴) 절을 가진 CNF 공식을 ₙ을 구성하였으며, 이들의 불만족 가능성은 일반 위치에 있는 n점 집합이 빈 볼록 육각형을 피할 수 없음을 의미합니다. 그런 다음 n = 30에 대한 불만족 증명이 17300 CPU 시간을 사용한 평행 컴퓨팅으로 SAT 솔버에 의해 발견되어, 빈 육각형 수 h(6)가 30과 같음을 의미합니다. 본 논문에서는 Lean 정리 증명기에서 이 결과를 형식화하고 검증합니다. 우리의 형식화는 이산 계산 기하학 아이디어와 유사한 Erdos-Szekeres 유형 문제에 성공적으로 적용된 SAT 인코딩 기법을 포함합니다. 특히, 우리의 프레임워크는 표준 수학적 객체를 명제 할당에 연결할 수 있는 도구를 제공하여, 다른 SAT 기반 수학 결과의 형식 검증을 위한 중요한 단계로 나타납니다. 전반적으로, 우리는 이 작업이 이산 기하 문제에 대한 방대한 계산이 사용될 때 검증의 새로운 표준을 설정하고, 수학 커뮤니티가 이 분야의 컴퓨터 보조 증명에 대한 신뢰를 높여줄 것이라고 희망합니다.