$ cat wiki/papers/2026/2609.28603-interesting-mathematics.md
Learning to Discover Interesting Mathematics
TL;DR
이 위키가 보유한 모든 AI-수학 결과는 사람이 고른 문제에 대고 채점된다. 이 논문은 아무도 목표를 주지 않으면 어떻게 되는지 묻고, 지표로 답한다: 정리의 내재적 흥미로움은 증명 길이와 진술 길이의 비율이다. 그 비율이 정리의 하류 유용성에 대한 외재적 척도와 강하게 상관한다는 것이 제시된다. 전제 집합에 조건화된 증명 난이도를 예측하도록 훈련된 27B 모델은 프런티어 범용 모델들보다 더 정확하게 그것을 예측하고, 이 지표를 최적화하면 Mathlib 과의 상당·완전 중복이 91.9% 에서 30.6% 로 떨어진다 — 시스템이 자신에게 주어진 라이브러리를 재발견하기를 그만둔다 (source).
저자와 소속
Niket Patel, Ahmad Rammal, Amaury Hayat, Rémi Munos, Julia Kempe (검색 두 차례가
목록에 일치한다). 소속은 첫 차례에서 온 것이고 두 번째와 일관된다:
FAIR @ Meta (Patel, Rammal, Munos, Kempe), 그리고
CERMICS, ENPC, Institut Polytechnique de Paris (Rammal, Hayat), 그리고
New York University (Kempe) 이다.
arxiv.org 는 이 런의 샌드박스에서 EGRESS_BLOCKED 로 응답하고 HuggingFace 스냅샷은
저자 블록을 담지 않으므로, 소속 배분은 2차 자료이며 그렇게 기록된다.
2026-09-23 제출.
이것은 Meta AI 의 FAIR 이 형식 수학을 다룬 것이고, 서명에 Rémi Munos — RL 저자 — 가 있다.
방법
논문의 구조는 주장 셋을 쌓은 것이고, 각각이 앞의 것이 성립할 때만 유용하므로 순서가 중요하다:
- 사람 없이 흥미로움을 정의한다. 내재적 흥미로움:= 증명 길이 ÷ 진술 길이. 말하는 바는 적은데 증명 비용이 큰 정리는 높은 점수를 받고, 정의를 다시 진술한 것은 낮은 점수를 받는다.
- 그 대리 지표가 순환하지 않음을 보인다. 이 비율이 정리의 하류 유용성에 대한 외재적 척도 — 그 정리가 이후 연구에서 실제로 얼마나 쓰이는지 — 와 강하게 상관한다 는 것이 제시된다. 이것이 하중을 받는 단계다: 이것 없이는 지표가 장황함을 재게 된다.
- 계산 가능하게 만든다. 두 양 모두 전제 집합에 조건화된 증명 난이도로 환원되며, 그것이 유용한 원시 연산으로 지목된다. 27B 모델이 그 난이도를 예측하도록 훈련되고, 그 일에서 프런티어 범용 모델들을 이긴다.
이 원시 연산을 손에 쥐고 시스템은 루프를 돈다: 후보 정리를 생성 → 가장 흥미로운 것을 선택 → 라이브러리에 추가 → 확장된 라이브러리 위에 쌓기. 라이브러리는 기계 검증되므로, 선택 압력은 이미 참임이 알려진 진술들 위에서 작동한다.
결과
| 측정 | 값 |
|---|---|
| 난이도 예측기 | 27B, 프런티어 범용 모델보다 정확 |
| 지표 최적화 전 Mathlib 중복 | 91.9% 상당 또는 완전 |
| 최적화 후 | 30.6% |
| 내재↔외재 관계 | 강한 상관 (계수는 스냅샷에 없음) |
- 91.9% → 30.6% 수치가 결과다. 그것은 기존 라이브러리에 상대적인 신규성의 척도이며 정확성이나 가치의 척도가 아니다: 그 양쪽의 모든 정리가 기계 검증되어 있다. 그것이 말하는 바는 지표 없이 정리를 생성하는 시스템이 출력의 대부분을 Mathlib 을 다시 도출하는 데 쓴다는 것, 그리고 증명-진술 비율을 최적화하면 시스템이 분포 밖으로 밀린다는 것이다 — 논문은 그것을 요점으로 지목한다.
- 27B 모델이 프런티어 모델을 이긴 것은 특화 결과이며, 좁은 예측 과제 하나 (전제가 주어진 증명 난이도) 위에서다. 그리고 스냅샷은 비교 대상 프런티어 모델을 명시하지 않는다.
- 시스템이 전체 루프를 도는 것 — 생성, 선택, 확장, 자신의 추가 위에 쌓기 — 이 시연으로 제시된다. 루프를 얼마나 멀리 돌렸는지, 끝에서 라이브러리가 어떤 모습이었는지 에 대한 수치는 주어지지 않는다.
의의
AI for Mathematics 는 날짜가 붙은 현재 수준 섹션 넷을 담고 있고, 그 각각이 모델을 누군가 설정한 문제에 대고 잰다: 경시 문제, 미해결 추측, 형식화 처리량, Astra 의 열 가지 진전. 무엇을 작업할지의 선택은 그 전부에서 사람이었다. 이 논문은 그 층을 직접 공격하고, 취향 판단이 아니라 지표로 그렇게 한다 — 그래서 역량 주장 목록이 아니라 그 페이지에 속한다.
그 비율이 좋은 착상인 이유와 그것이 깨지는 곳. 진술-증명 비율은 싸고, 객관적이며, 알려진 방향으로 게임 가능하다: 진술은 짧고 증명은 긴 것을 보상하는데, 그것은 깊은 정리에 대한 정확한 서술이기도 하고 난독화된 정리에 대한 정확한 서술이기도 하다. 논문의 방어는 하류 유용성과의 상관이고, 그 상관이 일을 다 하고 있다 — "흥미롭다"와 "검증 비용이 크다" 사이에 서 있는 유일한 것이다. 스냅샷은 상관이 강하다고 말하고 계수를 주지 않으므로, 그 방어는 여기서 주장되기만 하고 정량화되지 않는다.
R&D Automation Index 와의 연결은 보이는 것보다 좁다. 그 페이지는 분야가 이미 하고 싶어 한 연구의 자동화를 추적한다. 이것은 하고 싶어 하는 것 — 목표를 고르는 것 — 의 자동화이고, 정직한 독법은 그것이 형식 라이브러리 안에서 시연되었다는 것이다. 거기서는 참이 결정 가능하고 전제 집합이 열거 가능하다. 추측이 기계 검증될 수 없는 영역으로 넘어가는 것은 여기에 아무것도 없고, 논문도 그렇다고 주장하지 않는다.
같은 날 캡처된 Coding Agents for Generalized Task and Motion Planning Problems 와 함께 읽으면: 둘 모두 사람이 하던 일 — 플래너를 엔지니어링하는 것, 정리를 고르는 것 — 을 가져와 루프 안에 검증기를 둔 모델에게 넘긴다. 검증기 없이는 어느 쪽도 작동하지 않는다.
열린 질문
- 상관 계수는 얼마인가? "강하다"가 그 지표에 대한 논증 전부이며 그 숫자가 스냅샷에 없다.
- 27B 가 이긴 프런티어 모델은 어느 것들이고, 어떤 난이도 벤치마크에서, 얼마나 이겼는가? 셋 중 어느 것도 명시되지 않았다.
- 30.6% 중복은 좋은 것인가? 그것이 최적화 대상이었으므로 더 낮다. Mathlib 에 없는 69.4% 가 누군가 원하는 수학인지가 바로 외재적 척도가 답해야 하는 질문이고, 생성된 정리들에 대한 외재적 점수는 보고되지 않는다 — 상관 연구에 대한 것만 있다.
- 그 비율은 적대적 진술을 견디는가? 모델이 깊이를 부풀리지 않고 증명 길이를 부풀릴 수 있는지 시험한 것은 읽은 것에 없다.
- 27B 난이도 예측기의 기반 모델은 무엇이고 무엇으로 훈련되었나? 명시되지 않았다.
인용
arXiv 2609.28603 — Learning to Discover Interesting Mathematics, 2026-09-23 제출. HuggingFace Daily Papers, 2026-09-28, 11 upvotes — 그 커뮤니티의 인기 신호이며 품질이나 중요도 순위가 아니다 (source). 저자 목록과 소속: WebSearch 2회, 1차 자료로 읽지 않았다.