AI가 수학 난제 10건을 풀었다.. 이번엔 기계가 검증했다

오픈AI가 아직 내놓지 않은 모델로 수학 난제 10건을 풀었다고 8월 1일 밝혔습니다.

모델 이름은 '아스트라'입니다. 수학과 이론컴퓨터과학에서 10년 넘게 풀리지 않던 문제들입니다.

이런 발표는 처음이 아닙니다. 그래서 이번 건은 다른 데를 봐야 합니다.

작년에는 '심각한 왜곡'이라는 반박이 나왔다

오픈AI의 당시 과학 담당 부사장 케빈 웨일은 GPT-5가 에르되시 문제 10건을 풀었다고 했습니다.

에르되시 문제 데이터베이스를 관리하는 토머스 블룸은 이를 "심각한 왜곡"이라고 반박했습니다. 모델이 푼 것이 아니라 이미 나와 있는 논문을 찾아낸 것이었습니다.

그러니 "AI가 난제를 풀었다"는 말은 그 자체로는 근거가 못 됩니다.

오픈AI는 이번에 증명을 Lean 4 형식으로 만들어 깃허브에 공개했습니다. 라이선스는 아파치 2.0입니다.

Lean은 증명을 넣으면 컴파일되거나 안 되거나 둘 중 하나를 내놓습니다. 설득의 여지가 없습니다.

증명 파일에서 'sorry'를 찾으면 0건이라고 합니다. Lean에서 sorry는 "이 단계는 일단 넘어간다"는 표시여서, 0이면 빈칸 없이 다 채웠다는 뜻입니다.

모델을 믿을지 말지의 문제가, 컴파일러가 답하는 문제로 바뀐 셈입니다.

대표 결과는 '비소픽군'의 명시적 구성입니다. 미하일 그로모프가 1999년 소픽성 개념을 내놓은 뒤 27년간 열려 있던 질문입니다.

나머지는 콘 강성 추측 반증, 고차원 구 채우기 밀도, 이진·구면 부호, 산술회로 복잡도, 양자 병렬 반복 같은 영역에 걸쳐 있습니다.

10건을 푸는 데 든 토큰 값은 GPT-5.6 Sol API 요금 기준 약 2,000달러로 계산됐습니다.

다만 밀레니엄 문제는 풀지 못했습니다. 클레이수학연구소가 2000년에 꼽은 7대 난제로, 건당 상금이 100만 달러입니다.

논문 형태로 다듬은 것은 사람이 같은 모델과 함께 한 일이고, 수학적 논증 자체는 모델에서 나왔다고 오픈AI는 밝혔습니다.

경향신문 보도를 보면 이는 오픈AI만의 움직임이 아닙니다.

구글 딥마인드는 5월에 에르되시 문제 353개 중 9개를 풀었습니다. 7월에는 알파폴드 전담팀을 해체하고 인력을 제미나이 등으로 재배치해, 특화 모델에서 '범용 과학 에이전트'로 방향을 틀었습니다.

앤트로픽은 6월에 문헌 검색·코딩·데이터 분석·논문 초안을 한곳에서 처리하는 '클로드 사이언스'를 내놓고 소외질환 신약 후보물질 발굴에 나섰습니다.

오픈AI는 7월 30일 학술기관 연구자 10만 명에게 첨단 모델을 무료로 주는 계획을 발표했습니다.

이유는 여러 겹입니다. 경향신문은 회계 자동화가 일자리 감축 반발에 부딪히는 반면 신약·신소재는 '인류 복지'라는 명분이 서고, 국가전략과 맞물려 정부 지원을 끌어내기도 좋다고 짚습니다.

복잡한 연구 과정 자체가 모델 성능을 끌어올리는 시험장이 된다는 점도 있습니다.

돈도 따라옵니다. 머크는 4월에 구글 클라우드와 최대 10억 달러 규모 계약을 맺었고, 글로벌마켓인사이트는 AI 신약 개발 시장이 올해 40억 달러에서 2035년 439억 달러로 커진다고 봤습니다.

같은 보도에서 국내 상황도 나옵니다. 과기정통부가 7월에 AMD와 국가과학AI연구센터의 컴퓨팅 자원·인력 지원 협약을 맺었지만, 현재 인력은 20여 명 수준입니다.

비슷한 역할을 하는 캐나다 밀라연구소는 교수 140명에 학생 연구자가 1,200여 명입니다. 센터는 올 하반기에 인력을 더 뽑을 계획이라고 합니다.

그러면 독자에게 남는 것은 무엇일까요? 당장은 없습니다. 비소픽군이 우리 일에 쓰일 일은 없습니다.

다만 방식 하나는 가져갈 만합니다. AI가 내놓은 결과를 기계가 확인할 수 있는 형태로 받는 것입니다. 코드라면 테스트를 돌리고, 계산이라면 검산하고, 인용이라면 원문을 여는 식입니다.

"맞는 것 같다"와 "컴파일된다"는 다릅니다. 이번 발표가 앞의 실패와 갈린 지점이 정확히 거기였습니다.

8월 4일 기준으로 아스트라는 아직 나오지 않았고, 출시일도 가격도 공개되지 않았습니다.