수학을 위한 AI (AI for Mathematics)

정의

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

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

왜 중요한가

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

현재 수준 (2026-08-11)

기록이 0.000162 만큼 움직이고, AI 는 증명이 아니라 최적화기를 다듬는다 — AlphaEvolve, 2026-08-19. Improving the matrix multiplication exponent with modern optimization and AlphaEvolve (arXiv:2608.16884) 는 행렬 곱셈 지수 ω 의 알려진 최선 상계를 2.371339 에서 2.371177 로 개선한다. 세 단계다: combination loss analysis (Duan 외 2022, Williams 외 2024, Alman 외 2025 에 귀속되는 laser method 정련) 의 핵심에 있는 최적화 문제를 더 큰 설정에서 풀 수 있도록 재정식화하고, 그에 맞는 새 최적화 알고리즘을 설계한 다음, 그 알고리즘을 AlphaEvolve 로 다듬는다 (source).

역할 분담이 요점이고, 흔한 서사와는 정반대다. 여기서 AlphaEvolve 는 아무것도 증명하지 않는다. 사람이 재정식화하고 설계한 탐색 절차를, 사람이 정의한 공간 위에서, 앞선 세 논문이 세운 방법 안에서 다듬는다. 아래 항목들보다 좁고 읽기 쉬운 주장이며 — 그것들과 달리 검증 기계장치가 필요 없다. 이전 기록도 공개된 숫자이고 새 기록도 공개된 숫자다.

크기는 결과와 같은 호흡에 놓여야 한다. 상계는 0.000162 만큼 움직이고, ω 기록은 여러 해 동안 그 크기의 폭으로 움직여 왔으며, 논문 스스로를 note 라 부른다. 이것이 보이는 것은 잘 다듬어진 문제의 프런티어에서 도구가 기여할 수 있다는 것이지, 문제가 움직였다는 것이 아니다.

논문 페이지에서 가져온 유보: 저자나 소속이 읽히지 않았으므로, 이것이 Google DeepMind 의 논문인지 제3자의 AlphaEvolve 사용인지는 여기서 확정되지 않는다.

미공개 Claude — Anthropic, 2026-08-10. 리만 제타 함수의 비자명 영점 중 임계선 위에 놓인 것의 비율에 대한 증명된 하한이 41.6% 에서 67.2% 로 옮겨 갔다. 이 문제 역사상 최대 폭의 단일 개선으로 보고되었고, 수십 년의 인간 작업이 쌓은 수치를 밀어냈다. 결과는 증명이 공개된 채 Lean 으로 형식 검증되었고 이름이 밝혀진 외부 수학자(Brian Conrey, Dan Goldston)가 검토했다. Anthropic 은 이것이 완전한 증명으로 가는 길이 아니며 하한은 가설 자체에 도전하다 나온 의도치 않은 부산물이라고 밝힌다 (source).

이 페이지에서 검증이 공개되어 있고, 기계로 확인 가능하며, 연구소 자신의 설명과 독립적인 첫 항목이다. 아래에 서술한 생성/검증의 분리가 그것이 중요한 이유다. 회의적인 독자가 무언가에 대한 접근 권한을 받지 않고도 검사할 수 있는 여기 첫 결과다. 나머지 절반은 메커니즘이다 — 에이전트 하네스 안에서 아이디어 650개, 서브에이전트 약 60개, 셸 명령 2,400건, 출력 토큰 31M — 이는 모델이 증명을 뱉어낸 것이 아니라 사람이 돌릴 수 없는 규모의 탐색이라는 뜻이다. 자세한 내용은 More than two thirds of the zeros of the Riemann zeta function lie on the critical line 에.

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 의 세 번째 위험을 구체적으로 보여 준다.
• 공통 척도가 없다. 두 랩의 수학적 산출을 비교할 벤치마크도, 기준선도, 공통 문제 집합도 없다 — 서로 견줄 수 없는 결과 목록만 있을 뿐이다.

주요 논문

• Improving the matrix multiplication exponent with modern optimization and AlphaEvolve (2026-08, arXiv:2608.16884) — ω 상계 2.371339 → 2.371177; AlphaEvolve 는 결과를 증명하는 것이 아니라 최적화기를 다듬는다 → Improving the matrix multiplication exponent with modern optimization and AlphaEvolve (arXiv:2608.16884) (source)
• Claude / Anthropic, More than two thirds of the zeros of the Riemann zeta function lie on the critical line (2026-08-10) — 하한 41.6% → 67.2%, Lean 형식화가 anthropics/zeta-23-lean 에 공개, Brian Conrey 와 Dan Goldston 검토 → More than two thirds of the zeros of the Riemann zeta function lie on the critical line (source)
• 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 — 역량 주장으로 쓰이는 연구 산출