Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound
이 논문은 정확한 유리수 케이스 트리 인증서와 두 개의 독립적인 검증기(하나는 Python으로 구현되었고, 다른 하나는 Lean 4로 형식적으로 증명됨)를 도입하여 출판된 차단 데이터베이스에 있는 180개의 서로 다른 모든 그래프의 기하학적 비임베딩 가능성을 기계적으로 검증함으로써 최소 코헨-스펙커 경계의 결정적인 검증 격차를 메우며, 이를 통해 검증되지 않은 Z3 결정을 커널이 확인한 정리로 대체하는 동시에 기존 증명 파이프라인에 숨겨진 여러 결함과 불일치를 발견하고 해결한다.