Anthropic Claude, Lean 4 형식화로 지수 시간 가설(ETH) 반증

내부 연구용 Claude 모델이 n개 변수의 3-SAT 문제를 2^o(n) 시간 내에 해결하는 결정론적 알고리즘을 발견하여 지수 시간 가설(ETH)을 반증함
해당 알고리즘은 만족하는 할당의 개수를 세는 더 어려운 #3-SAT 문제를 2^(O(n log log n / sqrt(log n))) 시간 내에 해결함
결과는 순수하게 점근적이며 실제 현실의 수식들을 실용적으로 해결할 수 있음을 의미하지 않음
증명은 Lean 4 (v4.33.1)와 Mathlib를 사용하여 형식화되었으며 24개 가상 CPU에서 빌드 시간은 약 8분, 피크 메모리 사용량은 7GB임
핵심 아이디어의 압축된 설명을 바탕으로 Claude Opus 5.5(고 노력도)가 반증을 재파생할 수 있으나 이는 모든 delta > 0에 대해 3-SAT이 O(2^(delta n))에서 결정 가능하다는 것만 증명하고 더 정밀한 경계는 증명하지 못함
저장소는 Apache 2.0 라이선스를 적용받은 연구 산출물이며 유지보수되지 않고 기여를 받지 않음

핵심 내용