OpenAI, Lean으로 형식화한 열 건의 수학 성과: 내부 모델의 역할

8월 1일 OpenAI는 원고 「Ten Advances in Mathematics and Theoretical Computer Science」를 공개하고, 그 결과를 자사의 내부 모델에 돌렸다. 동시에 GitHub 저장소 `openai/ten-proofs`가 만들어져 열 건의 증명에 대한 Lean 4 형식화가 공개됐다. 결과 가운데 눈에 띄는 것은 구 채우기 지수의 개선 — 1978년 이후 처음이다 —, 비소픽(non-sofic) 군의 구성, 그리고 콘의 강성 추측에 대한 반례다. 저장소는 mathlib을 기반으로 한 Lean 4.32.0 프로젝트이며 Apache-2.0 라이선스로 공개됐다. 누구나 `lake exe cache get`과 `lake build All`로 증명을 다시 컴파일할 수 있고, ComparatorChallenges 폴더에는 독립적으로 검증하는 방법이 설명돼 있다.

언론은 이 결과들을 같은 8월 1일 OpenAI가 발표한 차기 모델군의 이름 「Astra」와 연결했다. 다만 원고가 말하는 것은 공개되지 않은 「내부 모델」뿐이다. 토큰 비용 약 2,000달러, 문서 249쪽 같은 수치는 제3자 보도에서 나온 것으로, 공식 발표 페이지는 현재 접근할 수 없다. 논문은 다시 읽어준 인간 수학자들에게 감사를 표하고, Shuoxing Zhou의 독립적이고 동시적인 연구를 언급한다. 그 연구는 일부 GPT-5.6 Sol의 도움을 받아 진행됐다.

SiliconANGLE에 따르면 수학적 논증은 모델에서 나왔지만, 그 산출물을 출판 가능한 원고로 만든 것은 인간 연구자들이었다. 그 다듬는 작업의 비중이 얼마나 되는지는 수치로 밝혀지지 않았다. Lean 4의 사용은 논점을 옮긴다. 인증서는 증명의 논리적 타당성을 보장하지만, 형식화된 명제가 역사적 미해결 문제와 일치한다는 것까지 자동으로 확인해 주지는 않는다. 그 확인은 여전히 사람의 몫이다. 열 건 가운데 정식 동료 심사를 통과한 것은 하나도 없다. 전례가 무겁다. 2025년 10월 GPT-5가 에르되시 문제 열 건을 「풀었다」는 발표는 근거가 없는 것으로 드러났고, erdosproblems.com을 운영하는 Thomas Bloom은 이를 심각한 왜곡이라고 규정했다. 반면 오늘의 열 건에 대해 같은 Bloom은 「big news」라고 말한다. 이론물리학자 Tobias J. Osborne이 지적하듯, 인용된 2,000달러는 성공한 토큰의 비용이지 시도 전체의 「수확」이 아니다. 이 점에 대해 OpenAI는 아무 정보도 내놓지 않았다. 이런 상황은 2026년 6월에 공개되고 the-decoder에 따르면 3,000명이 넘는 수학자와 국제수학연맹이 지지하는 「Leiden Declaration on Artificial Intelligence and Mathematics」— 투명성, 저작자 권리 보호, 결과에 대한 인간의 책임을 요구하는 문서 — 라는 맥락 속에 놓인다.

진짜 뉴스는 기계가 수학을 했다는 사실이 아니다. 그것은 몇 달째 이어지고 있다. 이번에는 결과 하나하나에 다시 컴파일할 수 있는 Lean 인증서가 따라온다는 점이다. 판단하기 위해 발표하는 쪽을 믿을 필요가 없다. 그러나 실패한 시도와 성공의 비율이 기업 비밀로 남아 있는 한, 이 모델들의 효율에 대한 평가는 통계라기보다 믿음의 문제로 남을 것이다.