수학을 위한 AI (AI for Mathematics)

정의

언어 모델을 써서 새로운 수학적 결과를 만들어 내는 일 — 가르치는 것도, 알려진 정리를 검색하는 것도 아니라, 문헌이 미해결로 남겨 둔 문제를 실제로 결판내는 것 — 그리고 만들어진 것이 옳은지 확인하는 데 쓰이는 별개의 장치.

이 분야는 그 이음매를 따라 갈라진다. 생성은 프런티어 모델의 역량이고, 긴 사고 사슬과 함께 추론 시점에 수행된다. 검증은 별개의 산물이다. Lean 4 같은 증명 보조기가 논증을 한 줄씩 기계적으로 다시 확인하며, 그것을 쓴 모델을 신뢰하지 않는다. 두 절반은 공급자도, 라이선스도, 실패 양상도 다르며, 이 둘을 뭉뚱그리는 것이 이 분야의 주장이 과장되는 주된 경로다.

왜 중요한가

• 모델이 정말로 새로운 것을 만들었는지 가릴 수 있는 가장 깨끗한 시험이다. 벤치마크 논쟁은 대개 하니스 구성 문제로 환원된다 — Eval Harness Configuration 참조. 미해결 추측에는 구성할 하니스가 없다. 증명이 서거나 서지 않거나 둘 중 하나다.
• 검증이 기계적이라는 점은 평가 분야에서 거의 유례가 없다. Lean 인증서는 모델도, 가중치도, 랩에 대한 접근 권한도 없이 노트북 한 대만 있으면 누구나 확인할 수 있다. 어떤 리더보드가 제공하는 것보다 강한 형태의 재현성이다.
• 페이싱 신호이기도 하다. 랩들이 벤치마크 점수 대신 연구 산출을 역량의 근거로 인용하기 시작했다 — Frontier Pacing 참조. 주장이 "어떤 지수에서 51점"에서 "1978년 이후 열려 있던 문제를 해결"로 옮겨 가면, 측정되는 대상도 그것을 확인할 자격이 있는 사람도 함께 바뀐다.

현재 수준 (2026-08-02)

Astra — OpenAI, 2026-08-01. 수학과 이론 컴퓨터과학의 결과 열 건이며, 각각 Lean 4 인증서와 사고 사슬 설명, 그리고 249쪽 원고를 동반한다. 명시된 결과로는 최초의 명시적 비소픽 군(non-sofic group), Connes' Rigidity Conjecture 의 반증, 일반적인 2인 얽힘 게임에 대한 양자 병렬 반복 정리, Ehrhart's volume conjecture, 그리고 1978년 이후 처음으로 개선된 고차원 구 채우기(sphere-packing) 일반 상한이 있다. 문제들은 최소 10년간 미해결이었다고 명시된다. 총 토큰 비용은 Sol API 가격 기준 약 $2,000 (source).

사람이 개입한 단계는 부수적이지 않다. Astra 공개에 대한 보도는 사람이 증명을 논문 형태로 정리한 뒤 Lean 인증서로 변환했다고 전한다 (source). 같은 분업이 앞선 결과에서도 나타난다. 2026-05-20 OpenAI 의 내부 추론 모델이 평면 단위 거리 추측(Erdős, 1946)을 반증했을 때, 전문 수학자들이 모델의 추론 기록을 읽고 핵심 아이디어를 추출해 간결한 형식 증명으로 다시 썼으며, 프린스턴의 Will Sawin 이 경계를 δ = 0.014 로 정교화했다 (source). 어느 쪽도 파이프라인 전체가 자율적이라고 보고되지 않는다.

5월과 8월 사이에 달라진 것은 규모와 확인 가능성이다. 결과 하나가 열이 됐고, 사람이 심사하던 산문이 기계가 확인할 수 있는 인증서가 됐다.

검증 도구는 열려 있고 생성 쪽은 그렇지 않다. Leanstral 1.5 (Mistral AI, 2026-07-01/02) 는 무료 API 엔드포인트를 갖춘 Apache 2.0 오픈 웨이트 Lean 4 정리 증명기다. 이 비대칭은 짚어 둘 만하다. 이런 논증을 생성하는 모델은 폐쇄돼 있고 Astra 의 경우 아예 출시되지도 않았는데, 그것을 확인하는 도구는 열려 있다.

탐색 기반 발견은 별개의 계보다. AlphaEvolve (Google DeepMind) 는 긴 추론이 아니라 평가자에 대해 점수가 매겨지는 프로그램을 진화 탐색해 수학·알고리즘 결과에 도달하며, 2026-07-10 Gemini Enterprise Agent Platform 에서 GA 에 이르렀다. Gemini 3.1 Deep Think 는 같은 랩 라인에서 추론 쪽에 해당하는 짝이다.

학계는 조건을 밝혔다. Leiden declaration on artificial intelligence and mathematics — 2026년 6월 공개, 국제수학연맹(IMU) 이 지지했고 Terence Tao, Peter Scholze, Kevin Buzzard, Scott Aaronson 등이 서명 — 은 다섯 가지 위험을 열거한다. 신뢰할 수 없는 결과, 누락된 인용, 폐쇄된 상용 시스템에 대한 의존, 과장된 주장, 그리고 과학적 독립성의 상실. OpenAI 는 Astra 글에서 이 문서를 인용한다 (source).

열린 문제

• Lean 인증서는 정리를 증명하지, 그 정리가 흥미롭다는 것을 증명하지 않는다. 형식화는 논증이 그 형식적 진술을 확립한다는 것을 확인해 준다. 그 형식적 진술이 수학자들이 관심을 두는 바로 그 진술인지는 확인해 주지 못한다 — 비형식적 추측에서 Lean 명제로 옮기는 번역 자체가 사람의 판단이고, 거기서 생긴 오류는 엉뚱한 것에 대한 기계 검증 증명을 낳는다.
• 동료 심사의 역할이 아직 정의되지 않았다. Lean 으로 확인된 논증은 동료 심사를 거친 논증이 아니며, 여기서 확인한 어떤 학술지 절차도 그것을 어떻게 다루는지 밝히지 않았다.
• 저작 표시가 미해결이다. 모델이 아이디어를 만들고, 수학자가 논문을 쓰고, 증명기가 확인할 때 그 결과를 어떻게 인정하고 인용하는지에 대해 여기서 확인한 관행은 없다 — Leiden 선언이 지목한 두 번째 위험이다.
• 주장을 독립적으로 재현할 수 없다. Astra 는 미출시다. 인증서는 누구나 확인할 수 있지만 생성은 OpenAI 바깥의 누구도 반복할 수 없으며, 이는 Leiden 의 세 번째 위험을 구체적으로 보여 준다.
• 공통 척도가 없다. 두 랩의 수학적 산출을 비교할 벤치마크도, 기준선도, 공통 문제 집합도 없다 — 서로 견줄 수 없는 결과 목록만 있을 뿐이다.

주요 논문

• OpenAI, Ten advances in mathematics and theoretical computer science (2026-08-01) — 249쪽 원고, GitHub 의 Lean 4 인증서 (source)
• OpenAI, An OpenAI model has disproved a central conjecture in discrete geometry (2026-05-20) — 평면 단위 거리 문제, Golod–Shafarevich 이론과 무한 유체론 탑을 경유 (source)
• Leiden declaration on artificial intelligence and mathematics (2026-06) — IMU 가 지지한 다섯 가지 위험에 대한 선언 (source)

관련 개념

• Reasoning Models — 파이프라인의 생성 쪽 절반
• Test-Time Compute (Inference-Time Compute Scaling) — 긴 사고 사슬 실행이 소비하는 것
• Eval Harness Configuration — 미해결 추측이 벤치마크 점수보다 깨끗한 주장인 이유
• Frontier Pacing — 역량 주장으로 쓰이는 연구 산출