수학을 위한 AI (AI for Mathematics)

정의

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

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

왜 중요한가

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

현재 수준 (2026-10-04)

이 페이지에서 가장 큰 결과가 30일 전에 발표되었고 오늘 읽혔다. Formalizing Fermat's Last Theorem (Anthropic Research, 2026-09-04, 주 저자 Tianyi Peng, Kevin Buzzard 자문)는 스스로를 이렇게 부르는 것을 보고한다

the first end-to-end, computer-checked proof of FLT.

(source)

항목	값
증명한 정리 수	30,300
최종 증명에 쓰인 정리 수	29,500
Lean 산출물	1,300만 줄
소요 기간	11일
출력 토큰	약 60억
모델	"a general-purpose internal research model roughly comparable to Claude Fable 5.1"
형식화는 "follows a simplified version of Wiles's proof from Darmon, Diamond, and Taylor"
이며, 사람의 수학적 개입은 "limited to occasional high-level instructions" 에 머물렀다.
인프라는 이름이 밝혀져 있고 Anthropic 것이 아니다: Prove2Me,
"an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University"
이며, 정리 진술의 유향 비순환 그래프(DAG) 를 유지해 여러 에이전트가 병렬로 작업할 수
있게 했다.

이것은 이 페이지의 ## 정의 가 세워져 있는 생성/검증 이음새의 가장 깨끗한 사례이고, 전적으로 검증 쪽에 속한다. FLT 는 1994년 Wiles 가 증명했다. 여기서 새로운 수학적 결과는 없다. 새로운 것은 1,300만 줄의 Lean 산출물 이 존재하고, 모델이나 가중치나 랩에 접근하지 않고도 누구나 노트북으로 다시 검사할 수 있다는 점이다. 아래의 nine-loop 결과 — 신규성 주장이 다투어지고 검증은 경쟁 랩의 모델에서 왔다 — 와 비교하면, 이쪽은 다툴 신규성 주장이 없고 검증이 기계적 이다. 서로 반대되는 득실이고, 이 페이지는 순위를 매기지 않고 둘 다 싣는다.

공개된 한계가 일반화되는 부분이고, 아래 절의 Claude-shaped science 가 지목하는 실패 양상과 일치한다:

likely much longer than it needs to be

간결한 피어리뷰 대안에 비해 그렇다는 것이며, 초기 에이전트 시도는

quickly lost track of the project's state and stopped collaborating effectively

실패한 반복을 통해 비보일러플레이트 줄의 약 7% 를 기여했다. 사람의 증명이 수백 페이지인 정리의 1,300만 줄 증명은 "도구를 만들기보다 계산을 갈아 넣는" 경향을 규모로 보여주는 것이며, 그것을 셀 수 있는 매체에서다.

명시되지 않았고 따라서 이 페이지에 없는 것: 비용, 이름이 밝혀진 공개 모델(연구 모델은 Fable 5.1 과의 비교로만 특징지어진다), 컴퓨트나 GPU 수치, 그리고 그 Lean 증명이 Lean mathlib 관리자나 학술지의 검토를 받거나 수락되었다는 어떤 진술도. "computer-checked" 는 증명 보조기에 관한 주장이고 피어리뷰에 관한 주장이 아니다.

포착 기록: +30일. 이 포스트는 anthropic.com/research 에 있고, 이 파이프라인이 2026-10-02 에 발견한 경로이며 그 실행은 이 포스트를 제목만으로 기록했다. www.anthropic.com 은 그 이후 모든 실행에서 1차 출처로 응답했으므로, 이것은 접근성 공백이 아니었다 — 아무도 요청하지 않은 경로였다.

현재 수준 (2026-10-02)

Anthropic의 연구 포스트 두 편, 그리고 둘이 합쳐 이 페이지에 처음으로 독립 교차 검증된 결과와, 모델이 무엇이 아닌지에 대한 가장 날카로운 진술을 준다.

9루프, 심사자가 아니라 경쟁 모델이 검증했다

Claude Science 플랫폼을 통한 Fable 5.1이 N=4 super-Yang-Mills 이론의 9루프 진폭을 계산했다. Lance Dixon이 2023년에 세운 8루프 기록을 넘어선 것이고, 원래의 bootstrap과 간접적인 form-factor 접근법 두 가지 서로 다른 방식으로 계산했다 (source).

이 결과를 이 페이지의 다른 모든 결과와 다르게 만드는 것은 검증이다. Song He의 그룹이 GPT-6의 도움을 받아 같은 답에 동시에 도달했다. 두 그룹, 두 랩의 프런티어 모델 둘, 하나의 답 — 위에 있는 어떤 자기 보고 벤치마크 수치보다 강한 확인이며, 산술에 대한 확인이고 새로움에 대한 확인은 아니다.

비용이 드물게 공개되었다: 총 "one or two thousand dollars", 그중 bootstrap만 "$100 of the budget, corresponding to running 96 CPUs for a week". 네 자리 수 금액으로 얻은 프런티어 물리학 기록이 자료이고, 루프 개수가 아니다.

게스트 저자가 자기 머리기사를 직접 깎아내리며, 이 페이지는 머리기사가 아니라 그것을 기록한다:

Instead, it did something it turned out humans were also able to do. Claude used known methods, with a bit more compute than people had tried to use before.

Dixon의 추가 코멘트가 반대 추를 제공한다 — "It's quite a triumph, in my opinion, for a large language model to execute all of the steps in the complicated recipe" — 따라서 이 페이지에서의 쟁점은 아무도 굳이 하지 않았던 지점까지 알려진 레시피를 실행하는 것이 수학적 결과인가 컴퓨트 결과인가이다. 여기서 해소하지 않는다.

"Claude-shaped science" — 협력자가 아니라 문제를 고르라

Matthew Schwartz, 게스트 포스트, 2026-10-01 (source). 논지는 문제 선택에 관한 것이다: 모델은 폭넓은 지식, 코딩, 수학이 과제에 필요한 것일 때 잘하며, 생산적인 수는 모델을 연구자로 세우는 것이 아니라 그런 문제를 찾는 것이다.

Claude and GPT are good at science, but they are not scientists: yes, they are smart, but it can take a lot of hand-holding to get them to produce anything of scientific value.

Claude Opus 4.5와 Claude Fable 5를 지명하며 보고된 규모: 타원 Feynman 적분 30개 — 15개 재현, 15개 신규, 세 달에 걸쳐 18개 분야 36편의 원고와 19명의 공저자, 경제학 논문 4,452편의 재현 패키지를 오픈소스로 전환, 상용 도구에서 옮긴 루틴 30,000개, AccStack 단어 강세 데이터베이스의 6,072개 언어와 그 참고문헌의 음운론 문헌 160,000건, 그리고 1000 Genomes Project에서 가져온 돌연변이 쌍 57억 개.

명시된 한계가 쓸 만한 부분이고, 그중 둘은 철학적이기보다 기계적이다: "Claude has no sense of time", 그리고 효율적인 도구를 만들기보다 계산을 갈아내는 경향 — 이는 구체적이고 확인 가능한 실패 양상이며, 9루프 결과가 알려진 레시피에 컴퓨트를 투입한 것으로 읽히는 이유다. 나머지는 긴 프로젝트에서의 컨텍스트 손실, 그리고 모델의 무엇이 과학적으로 흥미로운지에 대한 판단은 전문가 없이 신뢰할 수 없다는 것이다. 같은 포스트의 "15개 신규" 적분과 함께 놓으면, 둘은 모델이 사람이 고른 문제 안에서는 새로운 결과를 낼 수 있고 문제 자체는 고를 수 없다고 말한다.

현재 수준 (2026-09-28)

이 페이지의 모든 결과는 누군가 설정한 문제에 대고 채점된다. 이것은 문제의 선택을 최적화하고, 그것이 작동했다고 말해 주는 숫자를 보고한다. Learning to Discover Interesting Mathematics — FAIR @ Meta 가 CERMICS/ENPC 와 NYU 와 함께 (Niket Patel, Ahmad Rammal, Amaury Hayat, Rémi Munos, Julia Kempe; 2026-09-23 제출, 저자 목록은 검색 2회에서, arxiv.org 는 이 런에서 차단) — 정리의 내재적 흥미로움을 증명 길이 ÷ 진술 길이로 정의하고, 그것이 하류 유용성의 외재적 척도와 강하게 상관함을 보이며, 둘을 계산 가능한 원시 연산 하나로 환원한다: 전제 집합에 조건화된 증명 난이도. 그 난이도를 예측하도록 훈련된 27B 모델은 프런티어 범용 모델보다 정확하다고 보고된다 (source).

붙잡아 둘 만한 측정은 중복 수치다. 이 지표를 최적화하면 Mathlib 과의 상당·완전 중복이 91.9% 에서 30.6% 로 떨어진다 — 지표 없는 생성기가 출력의 대부분을 자신에게 건네진 라이브러리를 다시 도출하는 데 쓴다는 뜻이다. 그 수치의 양쪽 모두 기계 검증되어 있으므로, 그것은 정확성도 가치도 아니라 기존 라이브러리에 상대적인 신규성을 잰다.

왜 이것이 이 페이지의 역량 목록이 아니라 맨 위에 앉는가. 아래 필즈 메달리스트 25인의 선언은 "AI 벤치마크로 쓰이는 수학적 문제 풀이가 수학 자신의 필요와 어긋난다" 고 반론한다 — 분야가 푸는 것으로 측정되는데 원하는 것은 무엇을 증명할 가치가 있는가에 대한 판단이라는 것이다. 이것은 그 층을 선호가 아니라 숫자로 공격하는 이 페이지의 첫 항목이고, 그 루프가 사람이 준 목표 없이 도는 첫 번째다: 후보를 생성 → 가장 흥미로운 것을 선택 → 기계 검증된 라이브러리를 확장 → 그 확장 위에 쌓기.

한계 셋, 그리고 첫째가 논증 전부다. 내재적 비율과 하류 유용성 사이의 상관이 "흥미롭다"와 "검증 비용이 크다"를 가르는 유일한 것인데 — 증명-진술 비율은 깊은 정리와 난독화된 정리를 똑같이 보상한다 — 스냅샷은 상관이 강하다고 말하면서 계수를 주지 않는다. 둘째, 생성된 정리들에 대한 외재적 점수는 보고되지 않고 상관 연구에 대한 것만 있으므로, Mathlib 에 없는 69.4% 가 누군가 원하는 수학인지는 논문 자신의 기준으로도 답되지 않는다. 셋째, 방법 전체가 결정 가능한 참과 열거 가능한 전제 집합을 전제한다: 형식 라이브러리 안에서 시연되며, 기계로 확인될 수 없는 추측으로 넘어가는 것은 여기에 아무것도 없다. 논문도 달리 주장하지 않는다.

현재 수준 (2026-09-11)

필즈상 수상자 25 명이 AI 랩이 측정하는 것은 수학이 필요로 하는 것이 아니라는 선언에 서명했고, 반대의 대상은 기계가 아니라 벤치마크다. A Severe Misalignment of AI in Mathematics 는 2026-09-11 에 Terence Tao 의 블로그와 mathandai.org 에 게시됐고, 서명자는 25 명 전원 필즈상 수상자이며, 보도되는 수상 연도 범위는 1978 년부터 2026 년까지다 (인원수는 4 pass, 명단 열거는 1 pass). 이 페이지는 Leiden 선언이 그랬듯 추가 서명을 계속 받는다고 보도된다 (source).

제목의 단어가 정확한 일을 하고 있다. 주장은 수학 문제 풀이를 벤치마크로 쓰는 것이 "severely misaligned with the needs of mathematics itself" 라는 것이며 (2 pass), 이는 역량이 아니라 유인에 관한 진술이고, 결과가 틀렸다는 주장이 아니다. 명시된 메커니즘은 결과가 그대로 옮기면 "announced in a rush, leaving no time for a proper writeup, the isolation of new methods and ideas, and citing relevant previous work of others" (1 pass) 라는 것, 그리고 그 writeup 단계가 없으면 증명이 누구의 아이디어에 기대고 있는지 불분명해진다는 것이다 (source).

이 페이지 자신의 열린 문제가 그 두 절반을 모두 예고했다. "귀속이 해소되지 않았다" 와 "동료 심사의 역할이 아직 정해지지 않았다" 는 이 선언이 존재하기 전부터 여기에 Leiden 두 번째 위험으로 기록돼 서 있었다. 새로운 것은 진단이 아니라 누가, 몇 명이 말하는가이다 — Leiden 선언은 IMU 가 승인한 기관의 성명이었고, 이쪽은 이름을 밝힌 스물다섯 명, 그것도 그 분야에서 가장 많은 훈장을 받은 사람들이다.

이 위키가 이미 보유한 두 사건이 맥락으로 보도된다. 문서들은 Jacobian 추측 반례 — Anthropic 연구자 Levent Alpöge 가 Claude Fable 5 로, 동료 심사 없이 소셜 미디어에 발표 — 와 2026-09-08 Navier–Stokes 발표 및 Tristan Buckmaster 가 제기한 표절 문제를 든다. 후자는 이 페이지의 ## 상충 보고 에 기록돼 있다. 선언 자체가 그것들을 거명하는지는 2 pass 가 그렇다고 말하되 어느 pass 도 그 문장을 인용하지 않으므로, 연결은 문서들의 것으로 기록한다 (source).

선언이 무엇을 요구하는지는 여기에 기록하지 않는다. 읽지 못했기 때문이다. terrytao.wordpress.com 과 mathandai.org 가 이번 실행에서 모두 EGRESS_BLOCKED 라 전문을 연 적이 없고, 읽은 모든 소스가 우려를 서술할 뿐 요구도, 요청도, 권고 실무도 적지 않는다. 그 공백은 공백으로 둔다 (source).

그리고 같은 주가 "서두름" 이라는 지적에 대한 반례를 내놓았다. 2026-09-13 에 떠오른 An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics 는 IMO 2026 금메달 기준을 30/42 로 통과하고 체크포인트, 학습 데이터, 학습·추론 코드, 제출한 풀이, 새 벤치마크를 공개한다. IMO 점수는 선언이 반대하는 장르의 가장 순수한 사례 — 새로운 수학이 전혀 들어 있지 않은 대회 숫자 — 이면서, 동시에 이 페이지에서 가장 완전하게 문서화된 수학 AI 결과이기도 하다. 둘은 화해시키지 않고 나란히 기록한다 (source).

현재 수준 (2026-09-08)

두 그룹이 하루 차이로 강제항 유체 방정식의 유한 시간 폭발에 도달했고, 흥미로운 대목은 수학도 검증도 다툼의 대상이 아니라는 점이다. 2026-09-08 OpenAI 는 On the Navier–Stokes Millennium Prize Problem 을 공개하며, 최대 10,000개 에이전트를 약 88시간 병렬로 돌려 2026-09-05 에 도달하고 이어 약 17시간 의 Lean 형식화와 검증을 GPT-6 Astra 에 귀속시켜 얻은 강제항이 있는 3D Navier–Stokes 방정식의 유한 시간 폭발 증명을 보고했다(각각 3회·3회·2회 확인). 생성 모델은 내부용이며 미공개 라고만 서술되고, 연산 비용은 "수백만 달러대"(1회 확인)다. OpenAI 는 다른 그룹이 근접했다는 소문을 듣고 2026-09-01 에 착수했다고 밝힌다 (source).

그 다른 그룹은 같은 날 발표했다: Levent Alpöge(Anthropic)와 Tristan Buckmaster(NYU)가 매끄러운 강제항이 있는 유한 시간 폭발을 incompressible porous medium 방정식, 2D Boussinesq 방정식, 3D incompressible Euler 방정식에 대해 증명한 논문 셋을 올렸고, Córdoba 와 Martínez-Zoroa 의 작업 위에 세웠으며, 셋 모두 Lean 으로 검증하고 형식화를 공개했다. AI 의 역할에 대한 저자들 자신의 설명은 이례적으로 구체적이다: 선행 증명의 핵심 요소를 식별하고 그 논증을 재현하는 데 Claude, 본문을 작성하는 데 Claude 와 Codex (source).

이 페이지 정의의 검증 쪽 절반은 완벽하게 성립했고 생성 쪽 절반은 그러지 못했다. OpenAI 의 Lean 개발은 github.com/openai/NavierStokesAndEuler 에 공개되어 있고(Lean 4.34.0-rc2, Apache-2.0), 이번 실행이 직접 읽은 유일한 1차 산출물이다 — openai.com 과 cdn.openai.com 이 모두 여기서 차단되어 있기 때문이다. 그것은 양의 점성과 강제항 을 가진 ℝ³ 와 주기적 토러스 ℝ³/ℤ³ 위의 Navier–Stokes 폭발과, ℝ³ 위의 매끄럽고 컴팩트 지지를 가진 발산 없는 초기 속도 로부터의 Euler 결과를 형식화한다. README 는 이것들이 Clay 공식 서술의 대안 (C)와 (D) 에 대응한다고 밝힌다. 개발이 sorry 없이 완결되었는지에 대해서는 아무 진술도 하지 않으며, 이번 실행은 그것을 빌드하지 않았다 (source).

다투어지는 것은 출처이며, 이 페이지에서 특정 인물의 사적 데이터에 대해 그 질문이 제기된 것은 처음이다. Buckmaster 는 Sébastien Bubeck 이 일요일 통화에서 OpenAI 내부 모델이 이미 약 100쪽 짜리 증명을 만들었다고 말했고 Alpöge 를 저자에서 빼거나 OpenAI 에 주도권을 주는 발표 방식을 제안했다고 주장하며(2회 확인), OpenAI 도구에 넣어 온 자신의 사적 초고가 OpenAI 에 접근 가능했는지 공개적으로 묻는다(3회 확인). OpenAI 의 답변은 접근을 단정적으로 부인하고 영향의 부인은 유보하는, 서로 다른 일을 하는 두 문장이다. 두 문장 모두 Safety Monitoring and Data Retention 에 전문이 인용되어 있고, 보존과 접근을 소유한 것이 그 페이지이므로 여기서 되풀이하지 않는다. 이 페이지는 귀속 쪽 절반을 가진다 (source).

"귀속이 미해결" 은 이 페이지에 관행의 공백으로 적혔고, 분쟁이 되어 돌아왔다. 아래 열린 문제는 모델이 아이디어를 만들고 수학자가 논문을 쓰고 증명기가 검사할 때 결과를 어떻게 공로로 돌릴지 말하는 관행이 없다고 적는다. 이 페이지의 이전 항목들은 모두 연구소가 하나였고 경쟁 주장자가 없어서 그 공백은 이론적이었다. 여기서는 두 그룹이, 그중 하나에 경쟁 연구소 직원을 두고, 같은 주에 인접한 결과에 도달했고, 관행의 부재가 논쟁의 재료가 된다.

Terence Tao 는 Alpöge–Buckmaster 작업을 "remarkable achievement" 라 부르고 그 접근을 완전한 Navier–Stokes 문제로 확장하는 데 근본적 장애가 보이지 않는다고 말하면서(각각 1회 확인), AI 기업들이 오래된 수학 문제를 마케팅 증빙으로 쓰는 것을 개탄한다(2회 확인). 그의 블로그와 Mastodon 계정 모두 이 샌드박스에서 차단되어 있어 두 진술 모두 발췌를 통해 전해지며, 이 위키가 검증한 인용이 아니다 (source).

OpenAI 증명에 대한 독립적인 수학적 검토는 읽은 자료 어디에도 없다. 반응을 다루는 모든 발췌는 수학자들이 아직 그것을 보지 못했다 고 서술한다 — 원고의 호스트는 여기서 차단되어 있고, 원칙적으로 누구나 확인할 수 있는 Lean 인증서가 현재 검토에 열려 있는 유일한 부분이다. 그것은 이 페이지의 정의가 예측하는 형태 그대로다.

현재 수준 (2026-08-31)

조정자가 없는 에이전트 집단이 다섯 개의 미해결 문제에서 새로운 결과를 냈다 — Autonomous Mathematical Discovery in an Open-World Multi-Agent Environment, arXiv 2026-08-24. Autonomous Mathematical Discovery in an Open-World Multi-Agent Environment (Stephen Chung, Wenyu Du, William J. Wesley) 는 서로 다른 모델 계열에서 온 에이전트들이 the Station 이라는 환경에서 하나의 연구 목표를 공유하되 중앙 에이전트도 사전에 짜인 파이프라인도 없이 스스로 방향을 고르고, 실험하고, 협업하고, 이후 에이전트가 읽을 공유 문헌을 쓴다고 보고한다. 보고된 결과는 다섯 개의 미해결 문제에서 수학 문헌에 새로운 결과이며, 최초 발견은 Claude 에이전트에게 18 (64.3%), GPT 에이전트에게 9 (32.1%), Gemini 에이전트에게 1 (3.6%) 귀속된다 (source).

이 페이지의 다른 모든 결과는 한 연구소의 모델과 별도의 검사 장치를 짝지었지만, 이 결과는 그렇지 않다. OpenAI 의 열 가지 진전과 Claude 의 zeta 경계는 각각 닫힌 프런티어 모델을 사람의 편집 단계로 이어 붙였고, Lean 4 계열은 생성을 외부 prover 로 이어 붙인다. 여기서는 집단이 여러 계열이 섞여 있고 검증 아티팩트가 같은 환경 안에서 생산된 것으로 보고된다. 그것이 같은 수준의 보증인지가 질문이며, 그 부분을 읽을 수 없었다 — 이 실행의 샌드박스에서 arxiv.org 는 차단되어 있고, 이 페이지의 항목은 논문이 아니라 일치하는 두 번의 검색에 기대고 있다.

64.3% 는 이 위키를 포함해 가장 잘못 인용되기 쉬운 수치다. 각 계열의 에이전트가 몇이나 있었는지 밝힌 자료가 없으므로, 집단이 더 크거나 턴이나 예산이 더 많으면 역량이 같아도 최초 발견이 더 많이 나온다. 이는 Claude Opus 5 를 비롯한 무엇과도 역량 비교가 아니고, 버전 문자열도 공개되지 않았으며, 모델 페이지로 옮겨서는 안 된다.

그리고 이 결과는 아래 마지막 열린 문제에 정확히 내려앉는다. "공통 척도가 없다 — 견줄 수 없는 결과 목록만 있다"는 문장은 연구소들을 두고 쓰였다. 이 논문은 세 계열을 하나의 환경, 하나의 목표 위에 놓으며, 그것은 여기서 읽은 것 가운데 세 계열의 수학 산출물이 원리적으로나마 견줄 수 있게 되는 첫 배치다 — 그러고는 베이스라인도, 어블레이션도, 단일 에이전트나 조정된 집단과의 비교도 보고하지 않으므로, 그 배치는 검증된 것이 아니라 시연된 것이다.

현재 수준 (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 의 세 번째 위험을 구체적으로 보여 준다.

• 공통 척도가 없다. 두 랩의 수학적 산출을 비교할 벤치마크도, 기준선도, 공통 문제 집합도 없다 — 서로 견줄 수 없는 결과 목록만 있을 뿐이다.

• 이제 공동체가 그 척도 자체가 문제라고 말했고, 아무도 대안을 내놓지 않았다. 2026-09-11 선언은 수학 문제 풀이를 벤치마크로 쓰는 데 반대하고, 바로 위 항목은 벤치마크가 없다고 반대한다. 둘 다 참이면서 반대 방향을 가리키기에 모두 기록하며, 이번 실행에서 읽은 어떤 것도 둘을 화해시키지 않는다 (source).

• 자연어 전용 파이프라인에는 인증서가 아예 없다. An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics 는 탐색 루프 안에서 모델이 자기 증명을 검증하며 금메달 점수에 도달한다. Lean 인증서에 대해 이 페이지가 말하는 모든 것 — 모델도 랩도 없이 누구나 다시 검사할 수 있다는 것 — 이 여기에는 적용되지 않으며, 그 자연어 증명을 독립적으로 다시 읽었다는 보고도 없다 (source).

주요 논문

• 2026-09-23 — 문제의 선택을 최적화하는 이곳의 첫 항목. Learning to Discover Interesting Mathematics 는 흥미로움을 증명 길이 ÷ 진술 길이로 정의하고, 그 과제에서 프런티어 범용 모델을 이기는 27B 증명 난이도 예측기를 훈련하며, 그것을 최적화해 Mathlib 중복을 91.9% → 30.6% 로 줄인다. 하류 유용성과의 상관은 강하다고 주장되고 계수는 주어지지 않는다 (source)

• 2026-09-14 — 검토의 자동화된 절반에 증명된 사각지대가 있다. Beyond Solver Verdicts: Generative Reward Models for Autoformalization 는 Verdict-Preserving-Unfaithfulness 를 정의한다: 잘못된 형식화가 정상적으로 실행되고 기대한 판정까지 일치하는 경우로, 솔버는 인코딩을 인증할 뿐 그 인코딩으로의 번역은 결코 인증하지 않는다. 논문은 판정만 보는 구조적 휴리스틱이 그런 트레이스에서 우연 수준의 탐지에 묶인다는 것을 증명하고, 그 답으로 Generative Verification (GenV) 를 내놓는다 — 오프라인 Z3-equivalence 오라클을 참조 없이 쓸 수 있는 연속 점수로 증류한 것으로, 0.961 AUROC, 에이전트형 test-time compute 배분에서 후속 정확도 +11.3 포인트. Lean 4 가 아니라 Z3 이므로 아직 이 페이지 자신의 무대에는 닿지 않는다 (source)

• 2026-09-13 — 이 페이지에서 독자가 실제로 돌려볼 수 있는 첫 결과. An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematics 는 Nemotron 3 Ultra 와 두 개의 후학습 전문가 체크포인트로 생성 → 검증 → 정제 탐색을 돌리고 별도의 고연산 선택 단계를 두어 IMO 2026 에서 30/42, 명시된 금메달 기준을 기록한다 — 전 과정 자연어이며, 형식 증명기도, 외부 도구도, 인터넷 접근도 없다. 체크포인트 둘, 학습 데이터, 코드, 제출 풀이, 그리고 Nemotron-IMO-Bench(새 문제 200 개) 가 공개된다. 검증 절반이 없다: 아래의 다른 모든 항목은 생성에 Lean 인증서를 짝지우는데, 이것은 루프 안에서 모델이 스스로 검증한다 (source)

• A Severe Misalignment of AI in Mathematics (2026-09-11) — 필즈상 수상자 25 명이 서명한 선언으로, AI 벤치마크로 쓰이는 수학 문제 풀이가 수학 자신의 필요와 어긋난다고 주장한다; 이번 실행에서 본문은 읽지 못했다 (source)

• 2026-09-07 — 이 페이지의 열린 문제가 없다고 적어 둔 바로 그 관행에 대한 제안. Scores Alone Do Not Prove Discovery: The Discovery Certification Protocol for Auditing AI Research Agents 는 연구 에이전트의 발견 주장을 실행 가능한 복원 테스트 로 바꾼다: Gate 1 은 봉인된 평가에서 유용한 개선을 검증하고, Gate 2 는 짝지어진 에이전트들에게 등록된 출발 정보와 관측된 웹 콘텐츠를 주되 대상 연구 이력은 보류 하며, 수치 목표에 도달하는 모든 유효한 방법은 복원 증인을 제출하고 Core 거부권을 발동시킨다. 통제된 감사 두 건에서 96 에피소드 중 복원 0 회(상한 0.0468), 각 짝 연구에서 진실 피드백 복원 30 회 대 중립 복원 0 회, 그리고 결정론적이고 LLM 을 쓰지 않는 검증기 가 동결된 증거로부터 모든 판정을 재현한다. 소급 적용은 불가능하다 — 봉인과 등록은 작업 이전에 이뤄지므로 위에 기록된 분쟁에는 닿지 않는다. 다음에 올 발견들을 위한 제안이다 (source)

• OpenAI, Finite time blowup for Navier–Stokes 와 Finite time blowup for the Euler equation (2026-09-08) — Lean 4 인증서가 github.com/openai/NavierStokesAndEuler 에 Apache-2.0 으로 공개; 원고 자체는 이번 실행에서 읽을 수 없었다 (source)

• Alpöge 와 Buckmaster, incompressible porous medium·2D Boussinesq·3D incompressible Euler 방정식에 대한 매끄러운 강제항이 있는 유한 시간 폭발 논문 셋 (2026-09-08) — Lean 검증, 형식화 공개, 그리고 저자들이 집필의 어느 부분을 Claude 와 Codex 가 했는지 밝힌다 (source)

• 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 — 역량 주장으로 쓰이는 연구 산출
• Safety Monitoring and Data Retention — 2026-09-08 분쟁의 데이터 쪽 절반: 연구소가 사용자 세션에서 무엇을 보유하며, 무엇을 배제할 수 있는가

상충 보고

2026-09-08 Navier–Stokes 결과가 밀레니엄 상금 기준을 충족하는가. 두 설명이 유통 중이며 이 위키는 둘 사이에서 고르지 않는다 (source):

설명	주장	근거
보도	Clay 기준은 강제항 없는 방정식으로 정의되고 이 결과는 강제항이 있는 쪽을 다루므로, 상금은 미청구 상태로 남는다	검색 패스 2회
OpenAI 와 그 Lean 저장소	이 작업은 Fefferman 공식 서술 의 대안 (C)와 (D) 를 확립하며, 그 대안들은 명시된 감쇠·주기성 조건 아래 매끄러운 외력 을 가진 붕괴 예시를 허용한다	1차로 읽은 저장소 README, 그리고 원고를 인용한 패스 1회
두 사실이 어느 쪽 읽기와도 어색하게 놓이며, 화해시키지 않고 기록한다: **OpenAI 는
$1,000,000 상금을 추구하지 않겠다고 밝혔고**(2회 확인), **Clay 공식 서술을 집필한 Charles
Fefferman 은 "I was thrilled that the problem was solved" 라고 말한 것으로 인용된다**(1회
확인). 읽은 자료 어디에도 이 둘이 양립하는지에 대한 언급은 없다.

여기서 해소할 수 있는 분쟁이 아니다. 그것은 Fefferman 문제 서술의 문언 대 실제로 형식화된 정리에 달려 있고, 원고의 호스트는 이 샌드박스에서 차단되어 있다. Lean 개발은 공개되어 있으며, 그것이 이 문제를 판가름할 산출물이다.