🔢 mathematics

A Kernel-Checked Exclusion Certificate for Erd\H{o}s Problem 647

이 논문은 인수 분해 증거(factorization witnesses)를 체이닝함으로써 $n > 24$ 부터 $10^9$ 까지의 모든 경우에 대해 에르되시 문제(Erdős Problem) 647을 해결하는, Lean 4 기반의 공리 최소화된 완전 검증 증명을 제시하며, 이 결과의 신뢰성은 여러 독립적인 툴체인과 아키텍처 간의 바이트 단위 동일한 재현성을 통해 강화된다.

원저자: Ibrahim Mian, Shayaan Siddique

게시일 2026-08-19

📖 4 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Ibrahim Mian, Shayaan Siddique

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

수학의 광활한 풍경 속에는 겉으로는 단순해 보이지만 숫자 구조 내에 깊은 복잡성을 숨기고 있는 질문들이 존재합니다. 그중 하나는 수십 년 전 전설적인 수학자 폴 에르되시(Paul Erdős)가 제기한 것으로, 한 숫자와 그 약수 사이의 관계에 관한 것입니다. 모든 자연수는 자신을 나누어 떨어지게 하는 더 작은 숫자들의 집합을 가집니다. 예를 들어, 숫자 6은 1, 2, 3, 6으로 나누어집니다. 이러한 약수의 개수는 숫자마다 매우 다양하게 변합니다. 에르되시는 어떤 특정 패턴, 즉 어떤 숫자가 너무나 "풍부한" 약수를 가져서 더 큰 모든 숫자에 대해 특정 수학적 부등식이 성립하도록 강제하는 경우가 있는지 궁금해했습니다. 구체적으로, 그는 24보다 큰 숫자 중 특정 계산의 최댓값이 놀라울 정도로 작게 유지되는 숫자가 존재하는지 물었습니다. 오랫동안 컴퓨터들은 수십억 개의 후보를 확인하며 이 문제를 탐색해 왔지만, 그들은 단지 "아직 찾지 못했다"라고만 말할 수 있었습니다. 이러한 탐색는 강력하지만, 표준적인 컴퓨팅 방식에 의존하기 때문에 절대적인 수학적 확실성을 제공하지는 못하며, 아주 작은 의구심의 틈을 남겨두었습니다.

새로운 연구는 해결책을 찾아냄으로써가 아니라, 특정 임계값 아래에는 해결책이 존재하지 않음을 절대적인 확신을 가지고 증명함으로써 마침내 그 간극을 메웠습니다. 컴퓨터 과학자들과 협력한 연구진은 수학적 증명을 검증할 때 인간 수학자가 논증의 모든 단계를 확인하는 것과 동일한 엄격함을 갖추도록 설계된 특수 소프트웨어 시스템을 사용했습니다. 그들은 25에서 10억 사이의 숫자 범위에 집중했습니다. 문제를 수백만 개의 작고 검증 가능한 조각으로 나누는 방법을 사용하여, 그들은 이 방대한 구간의 모든 숫자에 대해 에르되시가 설명한 조건이 성립하지 않음을 입증했습니다. 이것은 숫자의 모습에 기반한 추측이나 숨겨진 오류가 있을 수 있는 시뮬레이션 결과가 아닙니다. 대신, 전체 추론의 사슬은 지름길이나 검증되지 않은 가정을 취하지 않고 논리가 제대로 유지되는지 확인하는 공정한 심판 역할을 하는 컴퓨터 프로그램에 의해 확인되었습니다.

이 성과의 핵심은 연구진이 이토록 넓은 범위를 커버하기 위해 필요한 방대한 양의 데이터를 처리한 방식에 있습니다. 그들은 시간이 너무 오래 걸리는 방식으로 모든 숫자를 개별적으로 확인하려 하지 않았습니다. 대신, 그들은 "증인(witnesses)"의 사슬을 만들었습니다. 강을 건너는 일련의 디딤돌을 상상해 보십시오. 만약 각 돌이 단단하다는 것을 증명할 수 있고 돌 사이의 간격이 충분히 좁다는 것을 증명할 수 있다면, 당신은 물에 빠지지 않고 강 전체를 건널 수 있습니다. 이 경우, "돌"은 특정 블록 전체에 대해 부등식이 성립하지 않음을 증명하는 특정 숫자들입니다. 연구진은 25부터 10억까지의 전체 구간을 덮기 위해 600만 개 이상의 증인을 생성했습니다. 각 증인은 수학적 조건이 깨지도록 강제함을 보여주기 위해 세심하게 분석된 숫자입니다. 이 작업의 탁월함은 컴퓨터 검증 시스템이 단순히 증인의 목록을 신뢰하는 것이 아니라, 각 속성을 처음부터 다시 계산하여 그것들이 유효하고 빈틈없이 완벽하게 결합되어 있음을 확인한다는 점에 있습니다.

결과가 단 하나의 잠재적으로 결함이 있는 컴퓨터 프로그램의 산물이 아니라는 것을 보장하기 위해, 팀은 표준적인 과학적 관행을 훨씬 뛰어넘는 교차 검증 시스템을 구축했습니다. 그들은 완전히 다른 언어로 작성되고 다른 방식을 사용하는 두 번째 컴퓨터 프로그램을 작성하여 증인의 전체 사슬을 재현했습니다. 이 독립적인 프로그램은 모든 단계를 확인하여 숫자들이 유효하고 논리가 타당함을 확인했습니다. 또한, 그들은 서로 다른 유형의 하드웨어와 서로 다른 소프트웨어 도구를 사용하여 전체 과정을 테스트했습니다. 그들은 별도의 기기에서 전체 시스템을 처음부터 다시 구축하여 최종 디지털 파일이 마지막 비트까지 동일한지 확인했습니다. 이러한 수준의 정밀 조사는 결과가 특정 기기나 특정 코드의 신뢰성에 의존하는 것이 아니라, 증명의 근본적인 논리에 기반하고 있음을 의미합니다. 연구진은 또한 해결책이 존재할 수도 있다고 시사했던 이전의 주장을 다루며, 이 새로운 엄격한 방법이 피했던 이전 시도의 논리에 결정적인 결함이 있었음을 보여주었습니다.

이 작업의 의의는 단순히 숫자에 관한 질문에 답하는 것을 넘어섭니다. 이는 결과의 신뢰성이 과정 자체에 내재되어 있는 새로운 방식의 수학을 보여줍니다. 과거에 컴퓨터가 복잡한 문제를 해결하는 데 사용되었을 때, 수학자들은 종로 종종 컴퓨터가 실수를 하지 않았는지 또는 코드가 버그로부터 자유로운지 믿어야 했습니다. 여기서 컴퓨터는 단순히 계산을 하는 것이 아니라, 의심의 여지가 없는 수준의 확실성을 가지고 계산을 검증하는 데 사용됩니다. 연구진은 25에서 10억 사이의 모든 숫자에 대해 에르되시가 설명한 조건이 성립하지 않음을 증명했습니다. 그들은 조건을 만족하는 숫자를 찾은 것도 아니고, 숫자의 세계에 그러한 숫자가 전혀 존재하지 않는다는 것을 증명한 것도 아닙니다. 그들은 단지 만약 그런 숫자가 존재한다면, 그것은 반드시 10억보다 커야 한다는 것을 증명했을 뿐입니다. 이는 10억 너머의 광대하고 미개척된 영역에 대한 가능성의 문을 열어두지만, 이전에 덜 확실한 방법으로만 확인되었던 전체 범위에 대해서는 문을 단호히 닫았습니다.

또한 이 연구는 작업에 사용된 도구를 검증할 수 있는 능력의 중요성을 강조합니다. 연구진은 자신들의 소프트웨어가 어떠한 숨겨진 가정이나 검증되지 않은 지름길에 의존하지 않도록 주의를 기울였습니다. 그들은 시스템의 핵심 논리로 검증할 수 없는 프로세스의 모든 부분을 제거했습니다. 이러한 접근 방식은 결과가 그것이 기반하고 있는 수학적 토대만큼 견고함을 보장합니다. 10억보다 큰 숫자를 향한 탐색이 다른 방법들을 사용하여 경계를 훨씬 더 멀리 밀어붙이고 있는 가운데, 이 작업은 그 범위에 대해 확실성의 토대를 제공합니다. 이는 수론이라는 추상적인 분야에서도, 논리의 다리를 구축하는 것이 가능하며, 그 다리가 매우 튼-튼하여 지나온 경로에 대해 의심의 여지 없이 완전한 확신을 가지고 건널 수 있음을 보여줍니다. 결과는 인간의 통찰력과 기계의 정밀함이 결래하여 달성한, 특정 거대 범위에 대한 오랜 질문에 대한 명확하고 확정적인 답변이며, 수학 연구에서 가능한 것의 새로운 기준을 제시합니다.

기술 요약: Erdős Problem 647에 대한 커널 검증 제외 증명서

문제 정의
Erdős와 Selfridge가 제기한 Erdős Problem 647은, $\max_{m<n} (m + \tau(m)) \le n + 2$ 를 만족하는 정수 $n > 24$ 가 존재하는지 묻는 문제입니다 (여기서 $\tau(m)$ 은 약수의 개수를 나타내는 함수임). 이 조건은 $n=24$ 일 때 성립하며 경계값 $n+2$ 는 타이트하지만, 더 이상의 해는 존재하지 않는다는 것이 추측되고 있습니다. 기존의 계산 탐색은 분할된 체(segmented sieves)와 모듈러 축소를 사용하여 $n \approx 9.17 \times 10^{18}$ 까지 해가 없음을 배제해 왔습니다. 그러나 이러한 계산들은 검증되지 않은 코드, 네이티브 decide такtik, 또는 문제 특화적인 공리들에 의존하고 있어, 형식 검증 시스템의 신뢰할 수 있는 증명 커널(trusted proof kernel) 밖에 놓여 있습니다.

방법론 및 증명서 설계
본 논문은 $24 < n \le 10^9$ 범위에서 해가 존재하지 않음을 배제하는 Lean 4 기반의 형식적 증명을 제시합니다. 이 증명은 모든 수의 완전한 소인수분해를 요구하지 않고도 효율적으로 체크될 수 있도록 설계된 "증인 체인(witness-chain)" 증명서 형식을 사용합니다.

증인 정의: 대상 $n$ 에 대한 "킬 위트니스(kill witness)" $m$ 은 $m < n$ 이고 $m + \tau(m) \ge n + 3$ 을 만족하는 정수로 정의됩니다. 이러한 증인은 구간 $[m+1, m + \tau(m) - 3]$ 내의 모든 $n$ 에 대해 해당 부등식을 반증합니다.
매끄러운 부분(Smooth Part) 최적화: 커널의 작업량을 최소화하기 위해, 증인은 완전한 소인수분해를 저장하지 않습니다. 대신 $m$ $m$ 을 나누는 모든 $p < 1024$ $p < 1024$ 인 소수의 최대 거듭제곱을 저장합니다.
- 커널은 저장된 소수 거듭제곱들의 곱이 $m$ 을 나눈다는 것을 검증합니다.
- 각 저장된 거듭제곱이 최대임을 검증합니다 (즉, $p^{e+1} \nmid m$ ).
- $\tau(m)$ 의 하한을 $\prod (e_i + 1)$ 로 계산합니다.
- 배가 규칙(The Doubling Rule): 만약 $m$ 의 나머지 인수(smooth part 이외의 부분)가 1보다 크다면, 해당 하한을 두 배로 늘립니다. 이는 나머지 부분이 smooth part와 서로소이므로, 존재한다면 적어도 두 개의 약수(1과 자기 자신)를 기여한다는 점에서 타당합니다.
- 나열된 소수( $< 1024$ )의 소수성은 31까지의 소수로 나누어 떨어지는지 확인하는 시정법(trial division)을 통해 검증하며, 별도의 외부 소수성 증명서를 필요로 하지 않습니다.
탐욕적 체이닝(Greedy Chaining): 증명서는 탐욕적으로 생성된 증인들의 시퀀스입니다. 커버 위치 24에서 시작하여, 알고리즘은 새로운 커버 위치 $m + \tau(m) - 3$ 을 최대화하는 증인 $m \le C$ 를 선택합니다. 이 6,685,922개의 증인 체인은 전체 구간 $(24, 10^9]$ 를 커버합니다.
형식화 구조: Lean 개발은 "타당성 계층(soundness layer, 체커의 로직을 증명)"과 "데이터 계층(data layer, 증인 리스트)"을 분리합니다. 데이터는 Lean 소스 파일에 리터럴로 인코딩됩니다. 커널은 체인의 연속성과 경계값의 유효성을 검증하기 위해 이 리터럴들을 평가합니다.

주요 기여 및 검증
본 논문은 다섯 가지 별도의 검증 및 기여 층위를 제공합니다:

공리 폐쇄(Axiom Closure): 최종 정리는 정확히 $\{ \text{propext}, \text{Classical.choice}, \text{Quot.sound} \}$ 라는 공리 폐쇄를 가지고 증명되었습니다. 여기에는 sorry, native decide, 또는 문제 특화적인 공리가 포함되지 않습니다.
독립적 재현(Independent Replay): 생성 스크립트는 명시적으로 신뢰할 수 없는 것으로 간주됩니다. 독립적인 파이썬 구현체가 시정법을 사용하여 모든 증인을 재현함으로써 소수성, 순서, 그리고 배가 규칙을 검증합니다. 세 번째 구현체는 $\tau(m)$ 을 독립적으로 재계산하여 솔루션 집합이 OEIS A087280과 일치함을 확인합니다.
소스로부터의 재현 가능성: 별도의 x86 하드웨어에서 gcc와 clang을 사용하여 Lean 툴체인을 소스로부터 컴파일하고, 캐시 없이 mathlib과 개발 결과물을 다시 빌드한 두 개의 독립적인 검증 단계가 수행되었습니다. 그 결과 생성된 .olean 파일은 원래의 ARM 빌드와 바이트 단위로 동일했으며, SHA-256 다이제스트 또한 일치했습니다.
단독 체크(Standalone Checking): 컴파일된 개발 결과물은 엘라보레이터(elaborator)를 우회하여 독립적인 lean4checker를 통해 재타입체킹되었으며, 이를 통해 컴파일된 아티팩트의 무결성을 확인했습니다.
결함이 있는 설계의 수정: 본 논문은 생성기가 큰 소수( $>1024$ )가 약수의 개수를 절반으로 줄이는 경우를 고려하지 못해 "간극 최소값(gap minimum)"에서 멈췄던 설계 반복 과정을 기록합니다. 배가 규칙을 포함한 최대성 및 배가 규칙을 도입함으로써 이 문제가 해결되었으며, 이는 건전성을 보존하는 강화 과정에서 "실패-명시(fail-loud)" 생성의 가치를 입증합니다.

결과
주요 결과는 정리 1.1입니다: $24 < n \le 10^9$ 인 정수 $n$ 중 $\max_{m<n} (m + \tau(m)) \le n + 2$ 를 만족하는 것은 존재하지 않습니다.

이 증명은 6,685,922개의 증인을 사용하여 구간 $(24, 10^9]$ 를 커버합니다.
$10^9$ 에 대한 증명서는 약 260 MB의 소스 코드로 구성되며, 버전 관리된 릴리스 아티팩트로 제공됩니다.
$10^7$ 및 $10^8$ 범위는 지속적 통합(CI)에 의해 강제되며, $10^9$ 범위는 clang 툴체인 하에서 한 번 커널 체크되었고 독립적 재현 파이프라인을 통해 검증되었습니다.

의의 및 범위
본 논문은 Erdős Problem 647을 종결짓거나, Idén, Hughes, bentrd 등의 연구자들이 도달한 $10^{18}$ 의 계산적 경지에 도달했다고 주장하지 않습니다.

신뢰 기반 vs 범위: 기여점은 **신뢰 기반(trust base)**이지 범위가 아닙니다. 이 결과는 $(24, 10^9]$ 범위에서의 비존재성 검증을 검증되지 않은 계산에서 커널이 체크하는 증명으로 전환했습니다.
유한 vs 점근적: 이 작업은 2026년 1월에 철회된 주장의 특정 간극을 다룹니다. 해당 주장은 모든 $n > 24$ 를 덮는 "지배 구간(domination intervals)"을 통해 문제를 증명하려 했으나, 구간들이 점근적으로 겹친다는 것을 증명하는 데 실패했습니다. 본 논문은 그 논증의 유한한 형태(유계된 범위를 덮는 것)가 증명 커널이 결정할 수 있는 체크 가능한 사실임을 보여줍니다.
미래의 한계: 저자들은 이 방법이 수학이 아닌 증명서 크기와 커널 시간에 의해 제한된다고 언급합니다. 범위를 $10^{10}$ 으로 확장하려면 약 2 GB의 소스가 필요하며, $10^{12}$ 는 불가능할 것입니다. 향후 작업은 선형 증인 체인이 아닌 구조적 논증(modular reductions)을 인증하는 방향이 되어야 할 것입니다.

요약하자면, 본 논문은 생성자의 신뢰성과 무관하게, 오직 Lean 커널과 표준 공리에만 의존하여 $(24, 10^9]$ 범위의 해가 존재하지 않음을 완전히 증명한 유한한 제외 증명을 확립함으로써 인증된 탐색의 새로운 표준을 제시합니다.

유사한 논문