GPT-6 아스트라, 리우빌 골드바흐 유사 추측 증명: Lean 검증 완료

수학자들은 아마도 AI의 환각을 세상에서 가장 참지 못하는 집단일 것입니다. 복잡한 수식 유도 과정에서 부호 하나만 삐끗해도 연구 전체가 무너지기 때문입니다. 하지만 그 증명 과정을 엄격한 형식화 증명 시스템에 통과시킬 수 있다면 이야기는 완전히 달라집니다.

연구자 Captain Sude는 깃허브를 통해 GPT-6 아스트라의 도움을 받아 리우빌 함수에 관한 골드바흐 유사 추측을 증명했다고 발표했습니다. 이번 연구의 핵심은 수학적 유도에 그치지 않고, 정리 전체를 대화형 정리 증명기인 Lean 4 코드로 작성해 빈틈없는 기계 검증을 마쳤다는 점입니다.

짝수를 '홀수 개의 소인수를 가진 두 수'로 분해하기

유명한 골드바흐 추측은 2보다 큰 모든 짝수가 두 소수의 합으로 표현된다는 명제입니다. 소수는 소인수가 자기 자신 하나뿐이므로 소인수의 개수는 당연히 홀수입니다.

이번에 해결된 정리는 골드바흐 추측의 유명한 유사 버전입니다. 정수론에서 리우빌 함수는 어떤 자연수의 소인수 총개수(중복 포함)가 홀수이면 -1, 짝수이면 1을 부여합니다. 이번 정리는 2보다 큰 모든 짝수 N이 리우빌 함수 값이 모두 -1인 두 양의 정수 a와 b의 합으로 나타낼 수 있음을 보여줍니다.

이 문제는 2018년 8월 Pablo라는 사용자가 수학 포럼 MathOverflow에 처음 질문을 올렸고, 이후 수학자 Mangerel의 논문에서 Shusterman의 연구로 귀속된 바 있습니다. 이전까지 Bloom의 스케일링 관찰과 Mangerel의 강성 및 교환 결함 논증 등이 디딤돌 역할을 해왔습니다.

아스트라는 두 개의 교환 대칭성과 강하법, 그리고 고전적인 이차 상호 법칙을 영리하게 결합하여 초등적인 증명 경로를 완성해 냈습니다.

Lean 4 검증 통과, 환각의 여지를 없애다

수학 연구에서 AI를 쓸 때 가장 두려운 부분은 그럴듯한 거짓말입니다. 하지만 연구자는 이 증명을 Lean v4.34.0-rc2 및 mathlib 환경에서 완벽하게 형식화했습니다.

빌드 로그와 공리 감사, 증명 경로 감사는 모두 결점 없이 통과했습니다. 최종 정리가 의존하는 것은 명제 외연성(propext), 선택 공리(Classical.choice), 몫의 건전성(Quot.sound) 등 Lean 커널의 핵심 논리 공리 세 가지뿐입니다.

코드 안에는 증명을 건너뛰는 'sorry' 키워드가 전혀 없으며, 임의로 추가된 검증되지 않은 수학적 공리도 존재하지 않습니다. 깃허브 액션을 통해 커밋할 때마다 새로운 빌드와 이중 감사가 자동으로 수행됩니다.

왜 중요한가

우리는 이번 성과가 프론티어 LLM과 형식 검증 도구가 결합했을 때 낼 수 있는 이상적인 연구 방식을 보여주었다고 생각합니다.

과거에는 AI가 수학적 진전을 이뤘다고 주장해도 전문가들이 몇 주 동안 달라붙어 환각을 가려내야 했습니다. 하지만 Lean과 같은 증명 보조기를 거치면 컴파일러가 논리적 무결성을 보증합니다. AI는 번뜩이는 아이디어로 증명 경로를 탐색하고, 기계는 논리적 오류를 철저히 차단하는 구조입니다.

수학 연구자들에게 이 워크플로는 이미 단순한 호기심 단계를 지나 실제 연구 동료 수준으로 진화하고 있습니다. 학술 포럼에 수년간 머물러 있던 미해결 문제를 기존 이론들을 엮어 초등적 증명으로 뚫어낸 것은 실질적인 진전입니다.

AI 업계 관점에서도 아스트라 같은 최상위 추론 모델이 단순 대화나 코딩 보조를 넘어, 엄격한 공리 체계 안에서 긴 호흡의 논리 연역을 완주할 수 있음을 입증한 중대한 이정표로 평가할 수 있습니다.