Five Formal Closures + Findings + AI-Generated Open Questions (Rei-AIOS Paper 118)

개요

Rei-AIOS Paper 118은 Lean 4를 사용하여 다섯 가지 독립적인 수학적 문제의 완전한 형식 증명, 관찰된 결과, AI가 생성한 새로운 개방형 질문, 그리고 D-FUMT₈ 해결 상태 요약을 제시합니다.

주요 내용

* 다섯 가지 형식적 증명 (Closures):
* 귀테 추측 (가환환): 가환환의 경우, 임의의 멱등 좌측 아이디얼의 합은 다시 멱등 좌측 아이디얼이 된다는 것을 Lean 4의 Mathlib 라이브러리를 사용하여 두 줄로 증명했습니다. 비가환환의 경우는 여전히 미해결 상태입니다.
* 문제 007: FIA 공리 독립성: D-FUMT₈의 8가지 값에 대한 폐쇄 대수(Fujimoto Infinity Algebra, FIA)의 6가지 공리가 상호 독립적임을 증명했습니다. 즉, 각 공리는 다른 5개 공리에서 도출될 수 없습니다.
* 문제 008: FDA ↔ Mathlib 생등 함수: 귀납적으로 정의된 DimensionValue 타입(FDA)과 Lean 4의 Option (Option ℤ) ⊕ Unit ⊕ Unit 타입 간의 생등 함수(bijection)를 구성하고, 양방향 정리를 증명했습니다. 이는 구조적 포함 관계를 보여주지만 FDA에 대한 대수 구조의 존재를 증명하지는 않습니다.
* 문제 013: C8 반복-경계 정리: 홀수 n에 대해 3 * (syrOne^[k] n) + 1의 2-p진 값(v₂)이 2 이상이 되는 k가 padicValNat 2 (n + 1)보다 작거나 같음을 증명했습니다. 이는 Collatz 추측의 특정 부분 궤적의 종료를 제한하지만, 전체 Collatz 추측을 해결하지는 않습니다.
* 문제 011: n=911 보편적 온램프: 25개의 "원자적 코어"(ATOMIC_CORES_25)로 정의된 특정 집합의 모든 홀수 n이 Collatz 궤적에서 n=911을 방문하며, 911에서 1까지의 꼬리 부분의 길이가 상수 K(911 → 1) = 41임을 native_decide를 통해 검증했습니다. 이는 25개 원소의 유한 집합에 대한 검증이며, 모든 홀수에 대한 일반화는 미해결 상태입니다.

* 결과 (Findings):
* 25개 원자적 코어 모두에서 n=911에서 n=1까지의 꼬리 길이가 정확히 41로 동일하다는 점을 발견했습니다.
* 9232 = 2⁴ · 577이라는 특정 피크 값이 188개의 다른 홀수 궤적(10⁶ 이하)에서 공유된다는 것을 발견했습니다.
* 피크 9232에 도달하는 모든 n의 직접적인 전조(predecessor)가 3077 = 17 · 181이라는 것을 확인했습니다.
* mod 96의 특정 나머지 클래스(HARD_96)에서 Oppermann 추측의 primeHi 구간은 기대치보다 +14.97% 많고, primeLo 구간은 -0.05% 적다는 비대칭성을 관찰했습니다.
* 특정 Collatz 극한값 n=27과 n=91이 mod 32에서 91 ≡ 27 (mod 32) 관계를 만족한다는 점을 관찰했습니다.

* AI 생성 개방형 질문: Rei-AIOS와 Claude Code가 공동으로 생성한 9개의 새로운 개방형 질문이 제안되었습니다. 이 질문들은 위에서 다룬 형식적 증명에서 자연스럽게 도출되었으며, 해당 특정 영역에서 AI가 제기한 최초의 공식 기록으로 여겨집니다. (예: 귀테 추측의 일반화 가능성, FIA 공리계의 최소성, FDA의 대수 구조 확장, Collatz 추측 관련 통계적 특성 등)

* D-FUMT₈ 해결 상태 요약: 각 문제와 질문에 대한 현재의 증명 상태(TRUE, FLOWING, NEITHER, BOTH)를 요약한 매트릭스를 제공합니다.

* 향후 연구 방향: 본 논문의 결과와 질문들은 "Rei Merge-Point Theorem", "비가환환 귀테 추측에 대한 가환환 도구 활용", "범주론적 D-FUMT₈" 등의 방향으로 나아가도록 시사합니다.

시사점

이 논문은 Lean 4를 사용한 엄격한 형식 증명의 적용 범위를 확장하며, AI가 수학적 탐구 과정에서 새로운 질문을 제기하는 데 중요한 역할을 할 수 있음을 보여줍니다. 제시된 개방형 질문들은 향후 관련 분야의 연구를 위한 구체적인 방향을 제시합니다.