Proof by Mechanization: Cubic Diophantine Equation Satisfiability is $Σ^0_1$-Complete

1. 연구 문제 (Problem)

수학의 제 10 문제 (Hilbert's Tenth Problem) 와 관련하여, 정수 계수 다항식 방정식의 해 존재성 (Diophantine satisfiability) 이 결정 불가능 (undecidable) 임은 MRDP 정리 (Matiyasevich, Robinson, Davis, Putnam) 를 통해 이미 알려져 있습니다. 그러나 **방정식의 차수 (degree)**와 변수의 수에 따른 결정 가능성의 경계는 여전히 활발히 연구 중인 주제입니다.

• 기존 결과:

  • 2 차 (Quadratic) 방정식: 일부 구조화된 형태는 결정 가능 (Hasse-Minkowski 등).
  • 4 차 (Quartic) 방정식: Jones (1980) 가 58 개의 변수를 가진 4 차 방정식이 모든 재귀 열거 가능 (r.e.) 집합을 표현할 수 있음을 보임 (보편성).
  • 미해결 문제: 3 차 (Cubic) 방정식의 경우, 단일 방정식 형태에서 모든 r.e. 집합을 표현할 수 있는지 (즉, $\Sigma^0_1$-완전성) 여부가 오랫동안 열려 있었습니다. Jones 는 3 차가 유일한 미해결 차수라고 명시했습니다.

• 본 논문의 목표:

  • 자연수 집합 $\mathbb{N}$ 위에서 정의된 단일 3 차 디오판토스 방정식의 만족 가능성 (Satisfiability) 이 $\Sigma^0_1$-완전 (즉, 결정 불가능) 임을 증명하는 것.
  • 이를 위해 **구체적인 보편적 3 차 다항식 (Universal Cubic Polynomial)**을 구성하고, 그 차수 한계를 기계적으로 검증하는 것.

2. 방법론 (Methodology)

저자는 수학적 증명을 Rocq (Coq 의 후속 버전으로 추정됨) 을 사용하여 기계화 (Mechanization) 했으며, 다음과 같은 3 단계의 계층적 구조로 증명을 구성했습니다.

A. 레지스터 산술 (Register Arithmetic, RA) 기반

• 약한 산술 체계: $I\Delta_0 + B\Sigma_1$을 제한하여 곱셈이 기본 연산이 아닌 $\Sigma_1$ 관계로 표현되는 **Register Arithmetic (RA)**을 사용했습니다.
• 이유: RA 는 유한 객체의 검증은 가능하지만, 모든 인스턴스에 대한 증명의 존재성을 보장하지는 않는 매우 약한 체계입니다. 이 "간극 (gap)"이 3 차 항이 발생하는 원인이 됩니다.

B. 증명에서 다항식으로의 컴파일러 (Compiler)

• 증명 검증의 다항식화: RA 의 증명 검증 과정 (공리 매칭, Modus Ponens 확인 등) 을 디오판토스 제약 시스템으로 변환하는 균일한 원시 재귀 컴파일러를 설계했습니다.
• 차수 제어 (Degree Control):
  • 구문 검증 및 추론 확인은 2 차 (Quadratic) 제약으로 컴파일됩니다.
  • 3 차 항의 발생: 선형 선택자 (selector, 1 차) 가 2 차 검증 의무 (quadratic obligation) 를 활성화할 때만 3 차 항 ($x \cdot y^2$ 형태) 이 발생합니다. 이는 "Guard Correctness" 기법을 통해 통제됩니다.
• 캐리리스 페어링 (Carryless Pairing): 피보나치 수열과 Zeckendorf 표현을 기반으로 한 페어링 함수를 사용하여, 비트 전파 (carry propagation) 없이 유한 시퀀스를 인코딩했습니다. 이는 다항식 제약의 차수를 낮게 유지하는 데 핵심적입니다.

C. 단일 방정식으로의 집계 (Aggregation)

• 시스템 축소: 여러 개의 3 차 제약 조건을 하나의 단일 3 차 방정식으로 합치는 혼합 기저 (Mixed-Radix) 집계 기법을 사용했습니다.
• 제약 조건: 각 제약 조건의 값을 기저 $B$의 자릿수로 간주하고, 가중치를 곱하여 합산함으로써 모든 제약이 동시에 만족될 때만 전체 식이 0 이 되도록 설계했습니다.
• 차수 보존: 제곱 (Sum-of-squares) 을 사용하지 않고 선형 결합과 용량 제약 (capacity constraints) 을 사용하여 최종 방정식의 차수가 3 을 초과하지 않도록 보장했습니다.

D. 기계화 및 검증

• Rocq (Coq) 구현: 컴파일러의 정확성, 차수 한계 ($\le 3$), 그리고 증명 검증과 다항식 해 존재성의 동치 관계를 Rocq 에서 완전히 검증했습니다.
• 구체적 생성: Python 생성기를 통해 실제 계수 테이블 (Coefficient Table) 을 생성하고, 이를 Rocq 에서 무결성 (Digest) 과 차수 증명을 통해 검증했습니다.

3. 주요 기여 (Key Contributions)

1. 3 차 단일 방정식의 $\Sigma^0_1$-완전성 증명:

   • 단일 3 차 디오판토스 방정식의 만족 가능성이 결정 불가능함을 증명했습니다. 이는 Jones 가 지적한 "차수 3 의 열린 문제"를 해결한 것입니다.
   • 기존 MRDP 정리의 "블랙박스" 축소와 달리, 직접적인 증명 - 다항식 컴파일러를 통해 차수 한계를 국소적으로 통제했습니다.

2. 구체적 보편적 다항식 (Explicit Universal Polynomial) 구성:

   • 9,692 개의 변수를 가진 단일 보편적 3 차 다항식을 명시적으로 구성했습니다 (Definition 6.1.1).
   • 이 다항식의 계수 테이블은 공개되었으며, Rocq 커널에 의해 차수 3 임이 기계적으로 검증되었습니다.

3. 기계화된 증명 (Mechanized Proof):

   • 증명 과정의 전 단계 (구문 분석, 증명 검증, 제약 생성, 집계, 차수 증명) 를 Rocq 에서 기계화하여 신뢰성을 확보했습니다.
   • 외부 의존성 없이 순수한 논리적 추론과 계산적 검증을 결합했습니다.

4. 차수 3 의 임계점 (Cubic Threshold) 에 대한 통찰:

   • 2 차는 표현력이 부족하고, 4 차는 너무 높은 차수인 이유를 설명했습니다.
   • 3 차는 "선형 선택자가 2 차 검증을 활성화"하는 메커니즘이 필요한 최소한의 복잡성을 가지며, 이는 자기 참조 (Diagonalization) 와 불완전성을 인코딩하는 데 필수적임을 보였습니다.

4. 결과 (Results)

• 정리 5.2.1: 단일 3 차 디오판토스 방정식의 만족 가능성 (CubicEqSat) 은 결정 불가능합니다.
• 정리 6.1.8 (유계 보편성): 주어진 자원 제약 (증명 길이 등) $k$에 대해, 해당 범위의 모든 RA 증명에 대해 해가 존재하는지 판단할 수 있는 유계된 3 차 다항식 $U_k$가 존재합니다.
• 정리 6.2.4 (고전적 보편성): 모든 자원 제약 $k$에 대한 유계 해의 합집합이 RA 의 전체 증명 가능 문장 집합과 동치임을 보였습니다.
• 구체적 데이터: Table 2 에 제시된 바와 같이, 최소 구성 (3 줄 증명) 과 효율적 구성 (1 줄 증명) 에 대한 구체적인 계수 테이블과 변수 수가 생성되었습니다.

5. 의의 및 중요성 (Significance)

1. 힐베르트 제 10 문제의 완성: 디오판토스 방정식의 결정 불가능성에 대한 차수별 분류에서 3 차라는 마지막 주요 격차를 메웠습니다.
2. 계산적 명확성 (Constructive Clarity): 기존의 존재성 증명 (Ontological proof) 을 넘어, 실제로 계산 가능한 계수를 가진 구체적인 다항식을 제시했습니다. 이는 이론적 가능성을 실험적으로 검증 가능한 형태로 바꿉니다.
3. 기계화 수학의 진전: 복잡한 논리 이론 (불완전성 정리, MRDP) 과 계산 복잡도 (Diophantine equations) 를 Rocq 에서 통합하여 검증함으로써, 수학적 증명의 신뢰성을 높이는 새로운 패러다임을 제시했습니다.
4. 불완전성과의 연결: 3 차 방정식의 임계점이 단순히 수학적 우연이 아니라, 논리적 자기 참조와 불완전성을 인코딩하기 위해 필요한 최소한의 계산 복잡도임을 보여주었습니다. 즉, "불결정성의 경계를 정의하는 것 자체가 그 경계를 넘어서는 행위"임을 시사합니다.

결론적으로, 이 논문은 3 차 디오판토스 방정식의 만족 가능성이 결정 불가능함을 기계적으로 증명하고, 이를 위한 구체적인 보편적 다항식을 구성함으로써 수리논리와 계산 이론의 오랜 난제를 해결한 획기적인 연구입니다.