한 개발자가 인공지능(AI)의 도움을 받아 50년 전 수학자 존 콘웨이(John Conway)가 제시한 '옴니픽 정수(omnific integers)의 정제(refinement) 추측'을 증명했다고 주장해 학계의 이목을 끌고 있습니다. 이 개발자는 수학적 지식이 부족함에도 불구하고, 대규모 언어모델(LLM)과 형식 검증 도구 '린(Lean)'을 활용하여 복잡한 수학 난제에 도전했으며, 그의 증명은 '팔로마 레지스트리(Palomar registry)'의 기계적 검증을 통과했습니다.
이 개발자는 AI에게 '초현실수(surreal numbers)' 분야의 미해결 문제를 찾아달라고 요청했고, AI는 콘웨이의 옴니픽 정수 추측을 제안했습니다. 옴니픽 정수의 정제 추측은 'ab = cd'일 때, 'a = ef, b = gh, c = eg, d = fh'를 만족하는 정수 e, f, g, h가 존재한다는 내용입니다. 개발자는 한 달간의 노력과 상당한 양의 AI 토큰(tokens)을 사용하여 린(Lean) 기반의 증명을 완성했으며, 이는 아직 독립적인 수학자들의 검증을 거치지는 않았지만, 린(Lean) 전문가들은 증명이 타당해 보인다고 평가했습니다.
이번 사례는 AI가 단순한 보조 도구를 넘어, 인간의 직관과 결합하여 복잡한 학술 연구를 수행할 수 있음을 시사합니다. 특히 수학적 배경이 없는 개인이 AI를 활용해 오랜 난제에 도전하고 유의미한 결과를 도출하려는 시도는, AI 시대에 지식 생산과 문제 해결의 패러다임이 어떻게 변화할 수 있는지를 보여주는 중요한 선례가 될 수 있습니다. 이는 학계뿐만 아니라 일반인에게도 AI를 통한 지적 탐구의 가능성을 넓혀줄 것입니다.