AI가 수학 난제 10개 풀었다, 단돈

OpenAI가 수학과 이론 컴퓨터과학의 오랜 난제 10개에서 진전을 냈다고 8월 1일 공개했습니다. 이 결과들은 아직 공개되지 않은 내부 모델 'Astra'가 만들어낸 것으로, OpenAI는 Astra를 '우리의 다음 주요 모델(next major model)'이라 소개했습니다. 다룬 문제들은 대부분 최소 10년, 길게는 수십 년간 핵심 결과에서 별다른 진전이 없던 것들입니다.

"이 문제들은 최소 10년 동안 핵심 결과에서 아무런 진전이 없었다."OpenAI

왜 중요한가

대상 분야는 고차원 기하, 부호 이론, 산술 회로 복잡도, 군론, 양자 복잡도, 격자 암호, 극단 조합론 등으로 넓습니다. 특히 검증 방식이 눈에 띕니다 — OpenAI는 249쪽 분량의 원고와 모델의 추론 과정, 그리고 10개 결과 전부에 대한 Lean 증명 인증서를 GitHub에 공개했습니다. 사람이 일일이 검토하는 전통적 동료평가 대신, 누구나 즉시·무신뢰(trustless)로 기계 검증할 수 있게 한 것입니다. 비용도 상징적입니다 — 10개 증명을 합쳐 약 2,000달러어치의 GPT-5.6 Sol API 토큰이 들었다고 합니다.

실무 적용

정답을 '기계가 검증 가능한 형식(Lean 등)'으로 강제하면, LLM의 그럴듯한 오류(할루시네이션)를 원천에서 걸러낼 수 있습니다. AI가 만든 산출물을 신뢰해야 하는 워크플로라면 '사람이 나중에 검수'가 아니라 '형식 검증을 파이프라인에 내장'하는 설계를 검토할 만합니다. 다만 형식 증명이 '맞다'는 것과 그 문제 설정·해석이 '의미 있다'는 것은 다른 문제이므로, 정식 동료평가는 아직 진행 중이라는 점은 유의해야 합니다.

교차 참고

• Simon Willison: Ten advances in mathematics and theoretical computer science — 결과와 Lean 검증이 갖는 의미를 정리한 관점을 함께 봅니다.
• BleepingComputer: OpenAI teases Astra after it solves 10 long-standing math problems — 미공개 모델 'Astra'의 위치와 맥락을 보완합니다.

Wemeet의 관점

Wemeet은 이번 발표의 진짜 뉴스가 '난제를 풀었다'가 아니라 '기계가 검증할 수 있게 풀었다'는 데 있다고 봅니다. AI의 주장을 사람이 믿어주던 시대에서, AI의 주장을 기계가 증명하는 시대로 넘어가는 신호입니다 — 신뢰의 근거가 '누가 말했나'에서 '검증 가능한가'로 옮겨갈 때, AI는 비로소 연구의 동료가 됩니다.