수학자, OpenAI의 추측 돌파를 24시간 만에 반박: 'AI가 모든 문장을 증명했지만, 더 이상 원래 추측에 대한 것이 아니다'

OpenAI는 자사의 차세대 AI 모델이 콘스 강성 추측(Connes rigidity conjecture)을 반증하는 것을 포함해 세계적인 수준의 수학 문제 10개를 풀었다고 주장했다. 다음 날, 한 인간 수학자가 AI의 반례가 유효하지 않다는 논문으로 대응했다. 캔자스 대학교 위상물리학센터의 J. L. 닐슨(J. L. Nielsen)은 OpenAI의 37,000줄에 달하는 Lean 4 코드를 처음부터 끝까지 추적하여 각 객체를 수학적 원형에 매핑하고, 두 가지 독립적인 실패 경로를 식별했다. 콘스 강성 추측은 두 군(群)이 동일한 연관 대수 구조를 갖고 두 가지 추가 조건(ICC와 카즈단의 성질 (T))을 만족하면 두 군은 동형이어야 한다는 것이다. OpenAI의 모델은 동일한 대수를 생성하는 두 개의 비동형 군을 구성했으며, 두 군 모두 ICC와 성질 (T)를 만족한다는 증명을 제시했다. 닐슨은 AI가 구성한 군 중 하나가 실제로 추가 조건을 만족하지 않으며, ICC도 성질 (T)도 아니라고 지적했다. 그녀는 세 가지 가능한 이유를 제시했다: 코드에서 성질 (T)의 표현이 카즈단의 원래 정의를 충실히 반영하지 못했거나, 증명이 군의 일부에 대해서만 성립하는데 전체 군에 적용되었거나, 코드 속의 군이 설명 문서에서 기술된 군과 다르다는 것이다. 닐슨은 또한 코드를 줄 단위로 검사하여 각 수학적 객체의 이름과 줄 번호를 상호 참조 표로 정리했다. 그녀는 ICC를 증명하는 데 사용된 보조 정리들이 이중 변환 후의 객체에 적용되었으며, 중심원소를 가진 원래 군에는 적용되지 않아 중요한 원소들을 직접 다루지 못한다는 것을 발견했다. 그녀는 자신의 두 가지 반박을 Lean 코드로 작성하여 Lean 4.32.2에서 컴파일했다. 논문의 마지막 섹션에서는 더 넓은 맥락을 논의한다: Lean 커널은 형식적 정확성을 보장하지만, 그 진술이 실제로 의도된 결론을 증명하는지는 보장하지 않는다. 테렌스 타오(Terence Tao)를 인용하면, 증명을 검증하는 것은 형식적 진술 자체를 확인하는 것이지 의도와의 일치를 확인하는 것이 아니므로 인간의 검토를 대체할 수 없다. 과거 다섯 가지 일반적인 Lean 벤치마크에 대한 감사에서 4,833개의 문제가 발견되었는데, 여기에는 반례, 공허한 정리, 신뢰할 수 없는 공리가 포함되었으며, 모두 기계로 검증되었지만, 나중에 인간이 반례를 구성하여 증명된 진술이 거짓임을 보여주었다. 닐슨은 OpenAI의 형식화가 주장하는 모든 결론을 올바르게 확립했을 수 있지만, 확립하지 못한 것—그리고 Lean 커널이 확인할 수 없는 것—은 이러한 결론이 원래 추측의 표현과 관련이 있는지 여부라고 썼다. 콘스 강성 추측은 여전히 미해결 상태로 남아 있다.