한줄 요약
OpenAI 수학 연구 결과가 8월 1일 공개됐습니다. 사내 모델로 미해결 수학·이론전산 문제 10개를 풀었고, 모든 증명에 기계가 자동으로 참·거짓을 판정하는 인증서를 붙였습니다.
무슨 일이 있었나?
OpenAI가 「Ten Advances in Mathematics and Theoretical Computer Science」라는 249쪽 논문과 함께, 증명 파일을 깃허브 저장소에 Apache 2.0 라이선스로 올렸습니다. 8월 1일 공개돼 지금(8월 4일 기준) 별 443개가 붙었습니다.
openai/ten-proofs 저장소 — Lean 증명 파일 목록과 Apache-2.0 라이선스
저장 소에는 결과별 .lean 파일이 하나씩 들어 있습니다. 언어 구성은 Lean 100%입니다.
푼 문제들이 가볍지 않습니다. 논문 초록에 적힌 10개 중 몇 개만 보면 이렇습니다.
- 비소픽 군의 구성 — 모든 가산군이 유한 순열로 근사되는지를 묻는 문제입니다. 이 개념은 그로모프가 1999년 논문에서 도입한 뒤 줄곧 열려 있었습니다
- 콘의 강직성 추측 반박 — 같은 폰노이만 대수를 갖는 서로 다른 군을 무한히 많이 구성해 추측을 무너뜨렸습니다
- 고차원 구 채우기 — 콘–엘키스 선형계획의 점근적 한계를 정확히 결정했습니다
- 다색 램지 수 — 에르되시 183번 문제를 해결했습니다
수학계 반응도 이미 있었습니다. 다만 여기서 자주 인용되는 필즈상 수상자 팀 가워스의 발언은 이번 10개가 아니라 그 전에 나온 별개 결과에 대한 것입니다. 평면 단위거리 문제 반례를 두고 한 말이에요. 가워스는 그때 "사람이 써서 Annals of Mathematics에 냈고 내가 의견을 요청받았다면, 망설임 없이 게재를 추천했을 것"이라고 했어요. 두 사건이 기사에서 자주 뒤섞이니 구분해서 보시는 게 좋습니다.
왜 중요한가?
성과 자체보다 검증 방식이 이 소식의 핵심입니다.
보통 새 수학 증명은 동료 심사를 거칩니다. 전문가 몇 명이 몇 달을 들여 읽고 판단해요. 그런데 이번 결과는 전부 Lean 4라는 증명 언어로 형식화돼 있습니다. Lean은 증명을 컴파일합니다. 통과하거나 실패하거나 둘 중 하나예요. 중간이 없습니다.
그래서 이 증명이 맞는지 확인하는 데 수학 박사학위도, 몇 달의 심사도 필요 없습니다. 저장소를 내려받아 돌려보면 끝입니다.
AI가 만든 결과물의 가장 큰 문제가 "그럴듯한데 틀린 것"이라는 걸 생각하면, 이건 그 문제를 우회하는 한 가지 방법을 보여준 셈입니다. 사람이 일일이 판단하는 대신, 검증 가능한 형식으로 답을 내게 만든 것이죠.
칠판 가득 적힌 수식
원문을 직접 확인하며 걸러낸 것 두 가지
이 소식은 여러 매체가 다뤘는데, 원문과 대조해보니 두 가지가 언론에서 덧붙여진 것이었습니다.
1. 모델 이름 "Astra"는 공식 자료에 없습니다. 여러 기사가 "OpenAI의 차기 모델 Astra"라고 썼지만, 249쪽 논문 전체에서 Astra라는 단어는 한 번도 나오지 않습니다. 논문은 시종일관 "an internal OpenAI model"(사내 모델)이라고만 씁니다. 이 모델은 아직 출시되지 않았고, 이름도 공식 확인된 바가 없습니다.
2. "약 2,000달러가 들었다"는 수치도 논문에 없습니다. 널리 인용되는 비용 수치인데, 논문 본문에서는 찾을 수 없었습니다. 별도 경로로 나온 이야기가 기사에 실린 것으로 보입니다. 인상적인 숫자일수록 출처를 따져봐야 합니다.
한 가지 더. 논문은 콘의 강직성 추측에 대해 다른 연구자가 독립적으로 같은 시기에 반례를 찾았다고 각주로 밝히고 있습니다. 그 연 구도 GPT-5.6 Sol의 도움을 일부 받았고요. AI가 혼자 진공 상태에서 해낸 일이 아니라, 사람과 AI가 같은 문제에 동시에 붙어 있었다는 뜻입니다.
실전에서 어떻게 쓸 수 있을까?
수학 난제는 우리 일과 멀지만, 여기서 가져올 원칙 하나는 그대로 씁니다.
AI에게 일을 시킬 때 "검증 가능한 형태"로 받아내는 것. 수학이 Lean으로 한 걸 우리 업무에 대입하면 이렇습니다.
- 숫자를 뽑게 했다면 계산식과 원본 데이터 위치를 함께 받기 — 결과만 받으면 확인할 방법이 없습니다
- 사실을 정리하게 했다면 문장마다 출처 링크를 붙이게 하기
- 코드를 짜게 했다면 테스트를 같이 짜게 하기 — 돌려보면 참·거짓이 나옵니다
공통점은 결과물 안에 자기 검증 수단을 넣는 것입니다. "이거 맞아?"라고 되묻는 대신 돌려보면 알게 만드는 쪽이죠.
인사이트
이번 발표에서 제일 눈여겨볼 대목은 OpenAI가 증명을 Apache 2.0으로 공개했다는 점입니다.
모델은 안 내놓으면서 결과물은 누구나 검증하고 가져다 쓰게 열어뒀어요. 보통 이런 발표는 "우리 모델이 이만큼 잘합니다"로 끝나는데, 이번엔 반박하고 싶으면 반박해보라는 형태로 나왔습니다. 실제로 Lean 인증서가 있으니 누구든 돌려서 확인할 수 있고요. 검증 가능성을 공개함으로써 주장의 신뢰도를 올리는 방식입니다.
그리고 이건 AI 발표를 읽는 우리 쪽 기준도 바꿉니다. 앞으로 "AI가 무엇을 해냈다"는 소식을 볼 때 물어볼 게 하나 생겼어요. 그래서 그게 맞는지 제3자가 확인할 수 있게 해놨나? 벤치마크 점수만 공개하고 재현 경로가 없는 발 표와, 검증 파일을 통째로 올린 발표는 같은 무게로 볼 수 없습니다.
공교롭게도 이번 소식 자체가 그 시험대였습니다. 모델 이름과 비용은 확인이 안 되는데 증명은 확인이 됩니다. 확인되는 것과 안 되는 것을 갈라서 읽는 게, AI 뉴스를 대하는 실용적인 태도 같아요.