GPT-6 Astra가 리우빌 버전 골드바흐를 해결했고, Lean이 독립적으로 재검증을 통과했다

동찰 Beating AI 속보, 익명 수학 커뮤니티 계정 Captain Sude가 GPT-6 Astra가 찾아낸 새로운 증명을 공개했으며, 이는 리우빌 버전 골드바흐 문제를 해결한 것이다.

이 문제는 고전 골드바흐 추측의 '두 소수'를 '두 소인수 총 개수가 홀수인 정수'로 완화한 것이다. 이전에 더럼 대학 수학자 Alexander P. Mangerel은 일반화 리만 가설이 성립하고 짝수가 충분히 클 때만 증명할 수 있었다.

Astra는 이제 이 두 가지 제한을 제거하여 2보다 큰 모든 짝수에 대해 성립함을 증명했다. 핵심 아이디어는 먼저 어떤 짝수가 이런 방식으로 분해될 수 없다고 가정한 뒤, 단계적으로 서로 모순되는 결과를 도출하는 것이다.

완전한 증명은 이미 Lean 4에 작성되었다. 프로젝트는 정상적으로 컴파일되며, 독립 감사 저장소에서도 성공적으로 재현되었고 `sorry`나 추가 수학 공리가 발견되지 않았다.

고전 골드바흐 추측 자체는 여전히 미해결인데, 여기서 두 가수는 여전히 합성수일 수 있기 때문이다.