The set of primes is supernatural: a Lean formalization of the statement of the conjecture

기술 요약: 소수의 집합은 초자연적이다: 추측의 진술에 대한 Lean 정식화

문제 정의
본 논문은 [3]에서 제안된 "초자연적 소수 추측(Supernatural Primes Conjecture)"의 정식화를 다룬다. 이 추측은 항등 함수와 상수를 사용하여 유한 번의 점별 덧셈, 곱셈, 거듭제곱을 통해 구성된 비상수 함수가 모든 양의 정수를 소수로 매핑할 수 없다고 가정한다. 본 논문의 목표는 이 추측과 그 주변의 이론적 틀을 Lean 4와 Mathlib 라이브러리를 사용하여 기계 검증 가능한 정식화로 변환하는 것이다. 목표는 이 추측에 대해 인간 및 자동화된 추론 시스템이 증명을 시도할 수 있도록 정밀하고 커널에 의해 검증된 타겟을 구축하는 것이다.

방법론
정식화는 전적으로 단일 Lean 4 파일인 SPCL.lean(약 1200행) 내에 포함되어 있으며, 오직 Mathlib에만 의존한다. 방법론은 [3]의 원본 논문을 Lean으로 직접적이고 철저하게 번역하는 것이며, 모든 정의, 예시, 비고, 번호가 매겨진 결과, 그리고 실험 테이블의 행이 기계 검증 가능한 대응물을 갖도록 보장한다.

주요 기술 구성 요소는 다음과 같다:

• 승연 구조(Elevation Structures): 논문은 덧셈, 곱셈, 거듭제곱의 호환성을 "승연 구조"(4-튜플 $(E, +, \times, \wedge)$)로 공리화한다. 이는 타입 클래스(type class)로 정식화되며, 항등 및 합성 법칙을 가진 이러한 구조들의 범주(category)가 구축된다.
• 자연 함수(Natural Functions): 두 가지 동등한 "자연 함수" 인코딩이 구현된다:
  1. 단어 구성(Word Construction): 함수들은 항등 함수와 상수 함수 집합에 적용되는 알파벳 $\{A_+, A_\times, A_\wedge\}$ 위의 유한한 단어들에 의해 생성된다.
  2. 귀납적 폐쇄(Inductive Closure): IsNatural이라는 귀납적 술어(inductive predicate)가 항등, 상수, 그리고 세 가지 연산에 대한 생성자를 통해 정의된다.
     두 정의 사이의 동등성은 정식으로 증명된다.
• 추측의 공식화: 추측은 증명 없이 Prop 타입의 이름이 지정된 명제(Conjecture_2_1)로 기술된다. 이는 sorry가 채워진 정리나 공리가 아닌 명시적인 가설으로 정의되어, 정식화가 새로운 가정을 도입하지 않음을 보장한다.
• 실험적 검증: 논문은 [3, §4]의 89개 실험 결과를 정식화한다. 이들은 특정 지점까지의 함수 값의 소수성(primality)과 첫 번째 비소수 값의 합성수성(compositeness)을 단언하는 정리로 기술된다.
  • 작은 값들에 대해서는 norm_num(계산적 평가)에 의존한다.
  • 큰 값들(예: $2^{2^6} + 93$)의 경우, 정식화는 루카스 소수 증명(Lucas primality certificates)을 사용한다. 이는 Mathlib의 reduce_mod_char 택틱을 사용하여 조건 $a^{p-1} \equiv 1 \pmod p$ 및 $a^{(p-1)/q} \not\equiv 1 \pmod p$ (여기서 $q$는 $p-1$의 소인수)를 확인하는 lucasCert 레마를 통해 검증된다.

주요 기여

1. 철저한 정식화: 본 논문은 [3]의 전체 내용을 완전한 "sorry-free" 정식화로 제공한다. 모든 정의, 레마, 명제, 테이블 행이 Lean 코드에 존재한다.
2. 정밀한 추측 타겟: 추측을 증명되지 않은 이름 있는 Prop으로 기술함으로써, 본 연구는 자동화된 추론 시스템을 위한 구체적이고 검증 가능한 목표를 생성한다. 의존 구조는 투명하다; 추측의 증명은 Lean/Mathlib의 정의와 공리에만 의존할 것이다.
3. 수학적 확장: 정식화는 더 넓은 함수 클래스인 IsNaturalKnuthFactorialSub를 정의함으로써 [3, Remark 3.4]의 이론을 확장한다. 이 클래스는 다음을 포함한다:
   • 커스(Knuth)의 업-애로우(up-arrow) 표기법 (여기서 화살표 레벨 자체가 클래스 내의 함수인 경우).
   • 계승(factorial) 함수.
   • 절단된 뺄셈 (조건 $g(n) < f(n)$ 하에서).
     논문은 원래의 자연 함수 클래스가 이 확장된 클래스에 임베딩됨을 증명한다.
4. 증명된 사례의 검증: 정식화는 추측이 알려진 대로 성립하는 경우(예: 비상수 다항식, 선형-지수 형태, 페르마 함수)에 대한 증명을 포함하며, 이는 Mathlib의 표준 수론적 결과(예: 다항식 가분성, 페르마의 소정리)를 활용한다.

결과

• 정식적 일관성: SPCL.lean 파일은 약 30초 내에 컴파일된다. 이는 Mathlib에서 상속된 Lean의 표준 고전적 공리(명제 외연성, 몫의 건전성, 선택 공리)에만 의존한다.
• 실험 테이블: [3]의 실험 테이블에 있는 89개 행이 모두 정리로 정식화되었다. 큰 소수성 주장에 대한 증명은 커널에 의해 검증된 루카스 증명서를 통해 검증되어, 인수 분해 문자열의 전사 오류 위험을 제거한다.
• 이론적 동등성: 정식화는 함수의 형식적 표현과 집합론적 재구성(소수의 집합이 "초자연적"이라는 것, 즉 무한한 자연 부분집합을 포함하지 않는다는 것) 사이의 동등성을 증명한다.
• 결과론적 함의: 추측이 성립한다는 조건 하에, 정식화는 합성 페르마 수의 집합이 무한하며, 임의의 비상수 자연 함수에 대한 비소수 값의 집합이 무한함을 증명한다.

의의
본 논문은 정식화의 엄밀성과 완전성에 그 주요 의의가 있다고 주장한다. 본 연구는 "[3]에서 설명된 것처럼 모든 종류의 지능에 대한 어려운 도전"을 정밀하고 기계 검증 가능한 타겟으로 변환한다. 모든 모호성을 제거하고 모든 단계가 Lean 커널에 의해 체크되도록 보장함으로써, 본 작업은 자동화된 추론 시스템이 밑바닥 정의의 인간적 오류 위험 없이 추측의 증명을 시도할 수 있는 기반을 마련한다. 논문은 추측을 해결한다고 주장하는 것이 아니라, 그러한 해결책을 검증할 수 있는 필요한 인프라를 제공하는 것을 목적으로 한다. 또한 Mathlib 생태계 내에서 복잡하고 실험적으로 유도된 수론적 추측을 정식화하는 것의 실현 가능성을 보여준다.