OpenAI ‘콘스 강성 추측’ 반례에 반박…“핵심 조건 충족 못해”

OpenAI가 차기 모델 ‘Astra’의 수학 성과로 공개한 콘스 강성 추측 반례에 대해 연구자가 핵심 가정이 충족되지 않았다는 반박을 제기했다. OpenAI 공식 발표와 연구자 제니 로레인 닐슨의 사전 논문을 대조하면, 양측의 쟁점은 형식 검증된 코드가 원래 추측의 적용 대상까지 정확히 포착했는지에 모인다.

OpenAI는 1일 수학과 이론컴퓨터과학의 장기 미해결 문제 10건에 대한 새 결과를 공개했다. 회사는 내부 버전 Astra가 결과를 찾았고, 사람이 모델과 함께 원고를 정리한 뒤 각 논증을 Lean 인증서로 형식화했다고 설명했다. 이 가운데 하나가 특정 군이 폰 노이만 대수에 의해 유일하게 결정된다는 콘스 강성 추측의 반례다. OpenAI는 공식 저장소에 관련 Lean 파일도 공개했다.

닐슨은 2일 공개한 사전 논문에서 이 반례가 추측의 전제 밖에 있다고 주장했다. 논문은 공개된 약 3만7천 줄의 Lean 코드를 검토한 결과, 반례 구성에 쓰인 군 가운데 하나가 무한 공액류 조건인 ICC와 카즈단 성질 (T)를 충족하지 못한다고 지적한다. 두 조건은 OpenAI가 다루려 한 강성 추측의 대상이 되는 데 필요한 핵심 가정이다.

반박 논문에 따르면 문제가 된 영 코사이클 군은 아벨 격자와 정수 심플렉틱 군의 직접곱 구조를 가진다. 이 구조에서는 중심에 비자명한 원소가 생겨 ICC 조건을 만족하지 못하고, 무한 아벨 군으로의 전사가 존재해 성질 (T)도 성립할 수 없다는 설명이다. 닐슨은 이 두 장애를 Lean 4로 별도 형식화했으며 오류나 미완성 증명 표시 없이 컴파일됐다고 밝혔다.

이번 논쟁은 Lean 코드가 컴파일됐다는 사실과 수학 명제가 원래 문제의 가정을 정확히 반영했다는 판단이 서로 다른 검증 단계임을 보여준다. 형식 증명 도구는 입력된 정의와 정리 사이의 논리적 일관성을 확인하지만, 형식화 대상이 연구자가 의도한 추측과 일치하는지는 별도의 수학적 검토가 필요하다.

다만 닐슨의 반박 역시 공개 직후의 사전 논문으로 동료평가를 거치지 않았다. PhilPapers 기록에는 아직 인용이나 후속 검증이 없고, OpenAI의 공식 답변도 확인되지 않았다. 따라서 현 단계에서 콘스 강성 추측의 반례가 최종적으로 무효라고 단정하기보다, OpenAI가 공개한 10개 성과 중 한 건에 구체적인 기술적 이의가 제기됐다고 보는 것이 타당하다.

OpenAI는 공식 발표에서 논문 작성과 Lean 형식화를 지원했으며 결과의 정확성에 책임을 진다고 밝혔다. 이번 반박에 대한 후속 설명과 공개 저장소 수정 여부, 독립 연구자들의 재검증 결과가 Astra의 수학 연구 역량을 평가하는 다음 기준이 될 전망이다.

출처: OpenAI 공식 발표 https://openai.com/index/ten-advances-in-mathematics/
출처: OpenAI 공식 논문 https://cdn.openai.com/pdf/ten-proofs-oai.pdf
출처: OpenAI 공식 Lean 저장소 https://github.com/openai/ten-proofs
출처: 제니 로레인 닐슨 사전 논문 https://philarchive.org/archive/NIEWTCv17
출처: PhilPapers 논문 기록 https://philpapers.org/rec/NIEWTC