니바 추측(Nivat's conjecture)과 AI: GPT-6 Pro가 찾은 Lean 증명, 그리고 '이해'가 더할 것

2026년 10월 28일, 수학자 Bryna Kra는 팟캐스트 Life, Automated¹에서, 모르는 사람들이 니바 추측(Nivat's conjecture)의 증명을 보내오기 시작했다고 말했습니다. 니바 추측은 Kra와 Van Cyr가 2012년에 주요 부분 결과 가운데 하나를 증명한 문제입니다. 에피소드 대본에 따르면 Kra는 "그리고 그 증명들은 옳은 것 같아요"라고 말했습니다. "문제는 풀렸지만, 거기에 무엇이 들어갔는지에 대한 이해는 전혀 없이 풀린 거예요."

적어도 하나의 증명 후보는 공개되어 있습니다. GitHub 저장소 boonsuan/nivat³에는 논문 한 편과 논증 전체의 Lean 형식화가 있습니다. README는 이렇게 말합니다. "증명은 전적으로 GPT-6 Pro가 내 프롬프트에 응답해 찾았다." 그리고 "Lean 형식화와 그에 딸린 문서는 Codex의 GPT-6 Astra Ultra가 만들었다." 형식화는 9월 14일, Lean 형식화 등록부인 Palomar에 등록되었습니다.¹⁰ README는 아직 일어나지 않은 일도 숨기지 않습니다. 논문은 "아직 사람이 수학적으로 소화하지 않았다"는 것입니다.

그래서 질문은 날카롭습니다. Lean 검사는 통과했지만 아무도 설명하지 않은 증명은 수학에 무엇을 줄까요? 아래에서는 추측이 무엇을 말하고 이전에 무엇이 알려져 있었는지, Kra가 무엇을 말하고 썼는지, 저장소에 무엇이 있는지, 그 Lean 증명이 무엇을 확립하는지, '이해'가 무엇을 더할지 정리합니다. 모든 출처는 2026년 10월 30일에 확인했습니다. 이름이 밝혀진 전문가가 이 증명을 확인했다는 공개 기록은 찾지 못했으며, Papex는 이 증명을 평가하지 않습니다.

니바 추측이란 무엇인가요?#

국소적인 다양성이 적으면 전역적인 반복이 강제된다는 추측입니다. Kra는 9월 테런스 타오의 블로그에 쓴 기고에서 이렇게 설명했습니다.

"정사각형 타일로 된 무한한 격자를 떠올려 보자. 각 타일은 빨강이나 파랑으로 칠해져 있다. 일정한 크기, 예컨대 가로 n칸, 세로 m칸인 직사각형 창(window)을 모든 위치에서 살펴보고, 그 창에 서로 다른 색 패턴이 몇 가지 나타나는지 센다. 추측에 따르면, 그런 패턴이 많아야 nm개라면 칠한 전체 모양은 격자의 어떤 고정된, 0이 아닌 이동에 대해 반복된다."²

색은 유한한 집합이기만 하면 됩니다. 빨강과 파랑은 예시입니다. 패턴의 개수를 패턴 복잡도(pattern complexity)라고 합니다. '반복된다'는 0이 아닌 이동 하나가 색칠 전체를 바꾸지 않는다는 뜻이며, 서로 독립인 두 방향으로 반복될 필요는 없습니다.

작은 예 두 가지가 왜 문턱이 정확히 창의 넓이에 놓이는지 보여 줍니다.

• 줄무늬. 열을 빨강과 파랑으로 번갈아 칠합니다. 두 칸 이상인 창에는 빨강 열에서 시작하느냐 파랑 열에서 시작하느냐에 따라 서로 다른 패턴이 두 가지만 나타납니다. 이 색칠은 한 행 위로 이동하면 반복됩니다.
• 튀는 타일 하나. 빨강 타일 하나만 빼고 모든 타일을 파랑으로 칠합니다. 창은 빨강 타일을 비켜 가거나(패턴 하나, 모두 파랑), 창의 nm개 위치 가운데 하나에 빨강 타일을 품습니다. 그러면 패턴은 nm + 1개이고, 어떤 이동이든 빨강 타일을 옮기므로 색칠은 결코 반복되지 않습니다.

그러니 넓이보다 패턴이 하나만 많아도 결코 반복되지 않는 색칠이 가능합니다. 추측은 넓이 이하에서는 이런 일이 일어날 수 없다고 말합니다.

1차원에서는 이에 해당하는 명제가 고전적인 정리입니다. Cyr와 Kra의 2012년 논문 초록이 상기시키듯, Morse–Hedlund 정리(1938)는 기호들이 무한히 늘어선 줄이 주기적일 필요충분조건은 어떤 n에 대해 길이 n인 서로 다른 블록이 많아야 n개라는 것이라고 말합니다.¹³ 니바 추측은 블록 대신 직사각형을 놓고 2차원에서 같은 것을 묻습니다. 위키백과에 따르면¹⁸ Maurice Nivat는 1997년 ICALP 학회에서 이 추측을 제안했고, Jarkko Kari와 Etienne Moutot는 이것을 "1997년에 제기된 이래 열려 있는" 문제로 묘사합니다.¹⁶

2026년 9월 이전에는 무엇이 알려져 있었나요?#

두 방향에서 나온 부분 결과들이 있었습니다. 하나는 동역학계를 통한 Cyr와 Kra의 접근이고, 다른 하나는 Kra의 말로 "조합론적 질문을 대수적 대상으로 보고, 특정한 종류의 다항식을 써서 무한한 패턴을 찾는" Kari와 Szabados의 접근입니다. 주요 결과를 각각 처음 공개된 해에 따라 정리하면 다음과 같습니다.

연도	결과	출처
2012	Cyr와 Kra: 패턴이 넓이의 절반 이하이면 주기적, P(n, k) ≤ nk/2	arXiv:1208.409013
2016	Kari와 Szabados: 점근적 판본. 주기적이지 않은 배치는 "유한히 많은 서로 다른 직사각형 모양에 대해서만" 복잡도가 낮다	arXiv:1605.0592914, ICALP 2015 논문을 확장
2017	Szabados: 주기적 배치 두 개의 합에 대해 추측이 성립	arXiv:1710.0536015
2019	Kari와 Moutot: 균일 재귀 배치(uniformly recurrent configuration)에 대해 추측이 성립	arXiv:1904.0126716
2026	Colle와 Garibaldi: 높이가 네 칸인 직사각형, P(4, n) ≤ 4n. 높이 3 이하에 대한 Cyr와 Kra의 결과를 확장	arXiv:2606.1019317

Kra의 기고는 두 방향이 왜 중요했는지 설명합니다. "같은 문제에 접근하는 서로 다른 두 방법은 우리에게 외치는 것 같았다. 둘 사이의 개념적 다리를 찾으라고. 우리는 시도했지만 성공하지 못했고, 다른 문제로 넘어갔다."² Kra의 표현으로는 "이 추측은 거의 30년 동안 우리의 노력에 저항했다".

Bryna Kra는 Life, Automated에서 무엇을 말했나요?#

에피소드 "Is Math a Canary in the AI Coal Mine? (with Bryna Kra)"는 KQED 사이트에 10월 28일 자로 올라 있습니다.¹ Life, Automated는 노스웨스턴 대학교 켈로그 경영대학원의 Ryan Institute on Complexity가 제작하고 KQED가 배포하며, 진행자는 Jess Love입니다. Kra는 노스웨스턴 대학교의 수학자이고, 페이지에 적힌 대로 미국수학회 회장을 지냈습니다. 페이지에는 대본과 함께 이런 안내가 있습니다. "이것은 컴퓨터가 생성한 대본입니다. 저희 팀이 검토했지만 오류가 있을 수 있습니다." 아래 인용은 이 대본에서 가져왔습니다.

증명이 도착한 경위. "그러니까 몇 주 전, AI 회사들이 새 모델을 내놓았을 때부터, 이 문제를 연구했던 우리는 증명을 받기 시작했어요. 그리고 그 증명들은 우리 중 누구도 모르는 사람들에게서 왔어요. 좋은 일이죠. 아시다시피 수학자들은 새로운 사람이 이 분야에 들어오는 걸 반기는 편이니까요."

빠져 있던 것. "글쎄요, 그 사람들은 결과가 어디서 왔는지 추적하는 데 아주 서툴렀어요. 그러니까 이전 결과에서 무엇을 가져다 쓰고 있는지요. 무엇이 새로운지도 강조하지 않았어요. 돌파구에 이르면 서론에 정말로 '이게 새로운 겁니다'라고 쓰고 싶어지잖아요." 그리고 "모든 걸 같은 무게로 놓는 셈이죠." 그다음에 이 글 맨 앞에 인용한 말이 나옵니다.

저자에게 묻기. "저는 그 사람들에게 답장을 써서, 그러니까 '만나서 증명을 설명해 주시겠어요?'라고 물었어요. 언제나 안 되는 이유가 있었어요." 그리고 "그중 한 명은 AI를 전면적으로 썼다고 밝혔어요. 그건 괜찮아요. 그러니까 자기가 한 일을 밝힌 거니까요. 그 사람들은 자기들이 수학을 잘 모르는 학부생이라고 했어요." Kra의 설명으로는 이것은 보낸 사람 한 명에 관한 이야기입니다. 에피소드는 아무 이름도 대지 않고 어떤 증명도 링크하지 않습니다.

두려워하는 것. "그게 한 일은 이 분야를 닫아 버린 거예요. 이제 누가 그걸 하나하나 따라가며 이해할 동기가 있겠어요? 어딘가 새로운 곳으로 이어지는 게 아니라면요."

Kra가 AI를 쓰지 않겠다고 말하는 것은 아닙니다. 같은 에피소드에서 Kra는 이렇게 말합니다. "읽다가 이해가 안 되는 게 있으면 써요. '이 명제에서 저 명제로 어떻게 넘어가는지 설명해 줘' 같은 걸 물어보기에 아주 좋은 방법이에요. 그런 걸 정말 잘해요."

Kra는 9월 테런스 타오의 블로그에 무엇을 썼나요?#

Kra의 기고 "Deep theorems were scarce and difficult and so became an effective mechanism to identify deep thought. AI has broken this system."²(깊은 정리는 드물고 어려웠기에 깊은 사유를 알아보는 효과적인 장치가 되었다. AI가 이 체계를 무너뜨렸다)는 9월 13일에 올라왔습니다.

"이번 주 나는 이 주제에 처음 발을 들인 연구자들로부터 추측 전체에 대한 증명이라는 것을 여러 편 받았다. 일부는 AI를 썼다고 밝혔지만, 영어를 다듬거나 증명을 확인하는 데에만 썼다고 했다. 저자들에게 Zoom으로 만나 논증을 설명해 줄 수 있는지 물었을 때, 초대를 받아들인 사람은 아무도 없었다."

Kra는 확인과 이해를 구분합니다. "그러나 AI 사용을 밝히고 증명이 옳은지 확인하는 것만으로는, 둘 다 꼭 필요한 일이지만, 요점을 놓친다. 이 결과들이 옳다고 해 보자. 그것은 수학적 기여다. 그런데 그것은 더 많은 질문을 연다. 우리는 무엇을 배웠는가? 저자들은 무엇을 기여했는가? 이 결과는 어떤 영향을 미칠 것인가?"²

그리고 증명이 무엇을 위한 것인지에 대해서는 이렇게 씁니다. "증명은 무언가가 참이라는 인증서 이상이다. 그것은 이야기이고, 그림이고, 통찰이고, 설명이다."

글은 AI가 만든 수학을 환영하면서("나는 AI가 생성한 증명을 환영하며, 사람만으로 만든 증명은 드물어질 것이라고 믿는다"), 무엇에 공로를 줄지 바꾸자고 요구합니다. "논문을 내는 것만으로는 더는 충분하지 않다. 저자는 증명의 작동 원리와 어떻게 거기에 이르렀는지를 설명할 수 있어야 한다. 학술지는 발견, 증명, 형식화, 설명의 역할을 구분하고 각각에 공로를 인정해야 한다."

두 설명은 한 가지 세부에서 다릅니다. 9월에 Kra는 AI 사용을 인정한 보낸 사람들이 AI를 "영어를 다듬거나 증명을 확인하는 데에만" 썼다고 썼습니다. 10월에는 보낸 사람 한 명이 AI를 전면적으로 썼다고 밝혔다고 말했습니다.¹ 두 출처 모두 두 설명이 같은 증명들에 관한 것인지는 말하지 않습니다.

boonsuan/nivat 저장소에는 무엇이 있나요?#

이 저장소는 9월 14일부터 GitHub에 공개되어 있습니다. 2026년 9월 14일 자 13쪽 논문 "Pattern complexity and Nivat's conjecture"가 있는데, 저자 표시에 GPT-6 Pro가 적혀 있고, 초록은 "우리는 니바 추측을 증명한다"로 시작합니다.⁷ mathlib 라이브러리 위에 세운 Lean 4 형식화("29개 라이브러리 모듈에 명시적 선언 377개가 있다"), 메타데이터 파일 formalization.yaml, 검사 로그도 있습니다. 9월 27일부터는 "Nivat's conjecture: an exposition of the GPT-6 Pro proof"도 있습니다.

저장소가 밝힌, 누가 무엇을 했는지는 다음과 같습니다(모델 이름은 저장소가 적은 그대로입니다).

부분	공로가 돌아간 곳	근거
증명 발견, 논문 작성	GPT-6 Pro	README3, 논문7, formalization.yaml4
Lean 형식화와 문서	"Codex의 GPT-6 Astra Ultra"(메타데이터 파일에는 "GPT-6 Astra", 프레임워크 Codex)	README3, formalization.yaml4
프롬프트, 방향 설정, 유지 관리	Boon Suan Ho	README3, formalization.yaml4
제출 전 검토	AI 에이전트, 상태 "agent-reviewed"	formalization.yaml4
해설을 위한 재작성(9월 27일)	Claude Opus 5.5	README3, 해설8
사람 전문가의 검토	주장하지 않음	README3, formalization.yaml4

관리자는 자기 역할에 대해 직설적입니다. "아래에서 강조하듯, 증명을 찾은 것은 GPT-6 Pro이지 내가 아니다. 내 역할은 모델에 프롬프트를 주고 형식적 검증을 마련하는 것이었다." 자기 한계에 대해서도 그렇습니다. "나는 이 분야의 전문가가 아니다. 나는 이 논증을 제대로 소화하거나 그에 걸맞은 해설을 쓸 자격이 있다고 보지 않는다". README는 다른 사람들을 초대합니다. "증명을 이해하고, 맥락을 짚고, 단순화하거나 설명하고 싶은 경험 많은 수학자들은 얼마든지 환영한다."³

사람의 확인에 관해, 9월 27일 업데이트는 해설에 대해 이렇게 말합니다. "원래 것과 마찬가지로 이것은 AI가 썼고 사람 전문가가 확인하지 않았다. 내가 아는 한, 사람이 소화한 증명 설명은 아직 없다." 메타데이터 파일은 이렇게 말합니다. "사람 전문가의 검토는 주장하거나 기록하지 않는다."⁴ 기록 자체의 한계도 적고 있습니다. "증명 생성 대화 기록은 포함되어 있지 않으므로, 공로 표시는 별도로 감사된 이력이 아니라 관리자의 공개 진술이다."

시점에 관해, 9월 14일 자 README 업데이트는 Kra의 기고가 "이 저장소에 내가 처음 커밋하기 약 3시간 전에 올라왔지만, 여기 보고한 증명 생성과 형식화 작업은 그 글을 알기 전에 마쳤다"고 말합니다. 블로그의 타임스탬프는 9월 13일 22:01 UTC이고,² GitHub는 첫 커밋을 9월 14일 01:44 UTC로 기록합니다.⁹

Kra가 받은 증명이 이것인가요?#

알 수 없으며, 찾은 출처 어디에도 그렇다는 말은 없습니다. Kra는 에피소드에서도 기고에서도 보낸 사람의 이름을 대지 않고 증명을 링크하지 않습니다. README는 이 증명을 Kra에게 보냈다고 말하지 않으며, 스스로를 "이 분야의 전문가가 아니다"라고 하는 관리자는 자신이 학생인지에 대해 아무 말도 하지 않습니다. Kra는 한 주에 "증명이라는 것을 여러 편" 받았다고 썼습니다.² 이 저장소는 공개된 후보 하나일 뿐, 반드시 Kra가 말한 학부생들의 증명인 것은 아닙니다.

Lean 증명은 무엇을 확립하나요?#

저장소는 Palomar의 관례를 따라 명제와 증명을 분리해 둡니다. README의 표현으로 Challenge.lean은 "증명 라이브러리와 독립적으로, mathlib 개념만 써서 명제를 진술하고", Solution.lean은 "바로 그 명제를 증명한다".³ 쉽게 말하면, 임의의 유한 알파벳과 정수 격자의 임의의 색칠에 대해, 어떤 양의 m과 n에 대해 모든 위치에서 센 서로 다른 m×n 패턴이 많아야 mn개라면, 0이 아닌 어떤 이동이 색칠을 바꾸지 않는다는 것입니다.

Palomar의 기록에 따르면 기계적 검증은 9월 14일 통과했습니다.¹⁰ Palomar의 소개 페이지에 따르면 Comparator 도구는 허용된 공리만 써서 "기록된 형식적 증명이 기록된 형식적 명제를 증명하는지 검증"하며, 증명은 Lean의 커널과 항목에 기록된 독립 커널들을 통해 다시 실행됩니다.¹¹ 이 항목은 NanoDa를 명시합니다. README는 증명이 Lean의 세 가지 표준 공리 propext, Classical.choice, Quot.sound만 쓴다고 말합니다.

이런 검사를 통과했다는 것은 한 가지 구체적인 뜻입니다. 형식적 명제가 Lean의 기초와 mathlib의 정의에서 따라 나온다는 것입니다. 그 단계에 대해서는 누구도 13쪽 논문이나 그것을 쓴 모델을 믿을 필요가 없습니다. 이것은 들리는 것보다 좁습니다. 네 가지는 사람의 몫으로 남습니다.

1. 이 명제가 니바 추측인가? 언어 모델이 수행하는 Palomar의 자동 편집 검토는 "선택된 정리는 내세운 유한 알파벳 직사각형 복잡도 함의와, 0이 아닌 단일 전역 주기라는 결론을 정확히 표현한다"고 판단했습니다. Palomar는 이 검토가 무엇인지 분명히 합니다. "이것은 결과를 수락하거나 승인하거나 보증하지 않는다. Palomar는 사람이 하는 편집 단계를 두지 않는다. 여기서는 아무도 심사위원처럼 수학을 읽지 않는다." Palomar의 보고서는 Challenge.lean을 40줄로 세는데, 전문가가 증명을 읽지 않고도 읽을 수 있을 만큼 짧습니다. 전문가가 읽었다는 공개 보고는 찾지 못했습니다.
2. 정의의 세부 사항. 명제는 mathlib의 Set.ncard로 패턴을 세는데, mathlib 자체 문서에 따르면 이 함수는 "s가 무한이면 쓰레기 값(junk value) 0을 취한다".¹² Challenge 파일은 여기서 이것이 왜 해가 없는지 설명합니다. "유한 알파벳과 유한 직사각형 때문에 이 패턴 집합은 유한하므로, 자연 기수는 의도한 개수 세기의 뜻을 갖는다."⁶ 이런 세부를 보라고 있는 것이 명제 감사이며, README는 "독립적인 명제 감사"를 요청합니다.
3. 논문. 메타데이터에 따르면 "Lean 명제의 형식적 검사가 비형식적 원고의 모든 문장을 검증하지는 않는다".⁴
4. 무엇이 새롭고, 누구의 것인가. 메타데이터는 "사람 전문가에 의한 독창성이나 우선권 평가는 주장하지 않는다"고 하며, GPT-6 Pro에 대한 공로 표시는 관리자의 공개 진술에 기대고 있습니다.

Palomar는 또 커밋 하나만, 즉 Lean 4.33.0용 9월 14일 빌드만 확인했고 그 보관 사본을 갖고 있습니다. 메인 브랜치는 그 뒤로 바뀌었습니다.

이 가운데 어느 것도 독자에게 정리가 왜 참인지 말해 주지 않습니다.

'이해'는 무엇을 더할까요?#

README는 테런스 타오에게서 어휘를 빌려 옵니다. "생성, 검증, 소화".³ 페이지 스스로 Claude가 초안을 쓰고 타오가 검토했다고 밝힌 타오의 견해 요약¹⁹은 소화를 "결과를 이해하고, 맥락 속에 놓고, 설명하는 것"으로 정의합니다. README는 프로젝트를 이 틀 안에 놓습니다. "이 프로젝트는 처음 두 활동을 다루며, 세 번째를 완료했다고 주장하지 않는다."

니바 추측의 경우, 소화는 Kra가 거듭 던지는 질문들에 답하는 일이 될 것입니다.

무엇이 새로운가? Kra는 자신이 받은 증명들이 "무엇이 새로운지 강조하지 않았다"고 했습니다.¹ GPT-6 Pro 논문은 초록에서 경로를 대략 그립니다. 알파벳에 유리수로 이름을 붙인 뒤 "직사각형의 넓이에 대한 귀납법을 쓰며", 격자 이동에 대한 다항식을 적용해 나가다가 "귀납법은 추측을, 두 차분 연산자의 곱이 c를 소멸시키는 경우로 환원하는데, 이 경우는 Szabados가 증명했다".⁷ Szabados의 2017년 논문은 스스로를 "Kari와 저자의 대수적 접근에 Cyr와 Kra의 균형 집합을 결합한다"고 설명합니다.¹⁵ 새 논증이 Kra와 Cyr가 찾던 "개념적 다리"인지, 다른 경로인지는 전문가들이 답할 질문입니다. 공개된 답은 찾지 못했습니다.

어디에서 왔는가? Kra는 자신이 받은 증명들이 "결과가 어디서 왔는지 추적하는 데 아주 서툴렀다"고 했습니다. 이 저장소는 출처를 기록합니다. 메타데이터는 Kari와 Szabados의 논문과 Szabados의 논문을 저장소가 "변형해 쓰는" 작업으로, Cyr와 Kra의 논문을 "배경"으로 표시합니다.⁴ 그 설명이 맞는지 역시 이 분야를 아는 사람들이 판단할 일입니다.

누가 질문에 답할 수 있는가? Kra는 기고에서 "질문에 답할 수 있는 능력"을 사람이 저자라는 것의 일부로 꼽습니다.² 관리자는 자신이 증명을 소화할 자격이 없다고 말합니다. AI가 쓴 해설은 있지만, 모델의 설명이 소화의 몫을 할 수 있는지는 열린 질문입니다. Kra 자신도 단계를 설명받는 데 AI를 쓰며, "이 수학에 대한 사람의 이해와 사람의 활용이 하는 역할은 매우 중요하다"고도 말합니다.

누가 할 것인가? Kra의 기고는 걸림돌을 짚습니다. "그 일에 보상이 없으면, 꼼꼼한 검증도 훌륭한 해설도 이루어지지 않을 것이다."

주장, 검증, 설명: 지금 어디에 있나요?#

앞서 쓴 글 OpenAI의 카케야, ETH, 양-밀스 주장: 무엇을 말하고 무엇이 아직 열려 있나는 발견, 검증, 설명이 이제 서로 다른 사람과 도구에게서, 서로 다른 날짜에 따로 도착한다는 점을 다뤘습니다. 10월 30일에 출처들이 밝힌 상태는 다음과 같습니다.

	상태	출처
주장됨	9월 14일 자 논문에 담긴 완전한 증명, 저자 표시에 GPT-6 Pro. Kra는 자신이 받은 증명들이 "옳은 것 같다"고 말함	저장소, KQED 대본1
기계로 확인됨	Lean 형식화. 9월 14일 Palomar의 기계적 검증 통과, 자동 검토에서 막는 문제 없음	Palomar 항목10
사람이 확인함	저장소가 주장한 것 없음. 이름이 밝혀진 전문가의 공개된 확인은 찾지 못함	README3, formalization.yaml4
설명됨	관리자가 아는 한 사람이 소화한 설명 없음(9월 27일). AI가 쓴 해설은 있으나 사람 전문가가 확인하지 않음	README3

어디에서 지켜볼 수 있나요?#

니바 추측은 Papex가 추적하는 미해결 문제 목록에 없으며, Papex는 이에 대한 주장을 추가하지 않았습니다. Papex는 추적하는 문제들에 관한 AI 활용 주장을 papex.org/ai-claims(영어)에 각 출처가 밝힌 그대로 링크와 함께 올립니다. 니바 추측의 경우 지켜볼 곳은 명제 감사와 해설을 요청하는 저장소³, 그리고 그 Palomar 항목¹⁰입니다.

열린 질문#

이 사례가 던지는 질문 가운데, 아직 정해진 답이 없다고 보는 것들입니다.

• AI가 찾은 증명의 형식적 명제는 누가 읽어야 하며, 다른 사람들이 기댈 수 있으려면 그 읽기를 어디에 기록해야 할까요?
• AI가 쓴 해설을 소화로 볼 수 있을까요, 아니면 소화에는 증명에 대한 질문에 답할 수 있는 사람이 필요할까요?
• 프롬프트를 준 사람, 증명을 찾고 형식화한 공로를 받은 모델, 그리고 언젠가 그것을 설명할 사람 사이에 공로를 어떻게 나눠야 할까요?
• 생성 대화 기록을 남기지 않으면, 공로 표시는 이 저장소의 말대로 "별도로 감사된 이력이 아니라 관리자의 공개 진술"이 됩니다. 작업을 하는 그 시점에 무엇을 남겨야 할까요?

저장소는 모델이 무엇을 했고, 관리자가 무엇을 했으며, 검사가 무엇을 다루고, 아직 아무도 하지 않은 것이 무엇인지 숨기지 않습니다. Kra의 기고는 마지막 부분이 왜 중요한지 말해 줍니다. "우리는 우리가 쓰는 것으로가 아니라, 우리가 배우고, 확인하고, 적용하고, 다른 사람에게 가르치는 것으로 수학을 발전시킨다."²

출처#

1. Is Math a Canary in the AI Coal Mine? (with Bryna Kra), Life, Automated (KQED, 2026년 10월 28일), 페이지와 컴퓨터 생성 대본, 2026년 10월 30일 확인 ↩ a b c d e
2. Bryna Kra, "Deep theorems were scarce and difficult and so became an effective mechanism to identify deep thought. AI has broken this system." (테런스 타오 블로그 기고, 2026년 9월 13일), 2026년 10월 30일 확인 ↩ a b c d e f g h
3. boonsuan/nivat, README (GitHub), 2026년 10월 30일 확인 ↩ a b c d e f g h i j k l
4. boonsuan/nivat, formalization.yaml, 2026년 10월 30일 확인 ↩ a b c d e f g h i
5. boonsuan/nivat, STATUS.md, 2026년 10월 30일 확인
6. boonsuan/nivat, Challenge.lean과 Solution.lean, 2026년 10월 30일 확인 ↩
7. Pattern complexity and Nivat's conjecture (paper/nivat.tex, 2026년 9월 14일 자, 저자 표시 GPT-6 Pro), 2026년 10월 30일 확인 ↩ a b c
8. Nivat's conjecture: an exposition of the GPT-6 Pro proof (paper/exposition.tex, 2026년 9월 27일 자, 저자 표시 Claude Opus 5.5), 2026년 10월 30일 확인 ↩
9. boonsuan/nivat, 커밋 이력 (GitHub), 2026년 10월 30일 확인 ↩
10. Palomar 항목 PALOMAR-2026-09-14-000003, 버전 1, 항목 기록과 공개된 검토 포함, 2026년 10월 30일 확인 ↩ a b c d
11. About Palomar (Palomar 등록부), 2026년 10월 30일 확인 ↩
12. Mathlib, Mathlib/Data/Set/Card.lean (GitHub), 2026년 10월 30일 확인 ↩
13. Van Cyr, Bryna Kra, Nonexpansive Z^2 subdynamics and Nivat's conjecture (arXiv:1208.4090, 2012), 2026년 10월 30일 확인 ↩ a b
14. Jarkko Kari, Michal Szabados, An Algebraic Geometric Approach to Nivat's Conjecture (arXiv:1605.05929, 2016), 2026년 10월 30일 확인 ↩
15. Michal Szabados, Nivat's conjecture holds for sums of two periodic configurations (arXiv:1710.05360, 2017), 2026년 10월 30일 확인 ↩ a b
16. Jarkko Kari, Etienne Moutot, Decidability and Periodicity of Low Complexity Tilings (arXiv:1904.01267, 2019), 2026년 10월 30일 확인 ↩ a b
17. C. F. Colle, E. Garibaldi, A Modular Structure Theorem for Minimal Periodic Decompositions and Periodicity of Configurations with P(4,n) ≤ 4n (arXiv:2606.10193, 2026년 6월), 2026년 10월 30일 확인 ↩
18. Nivat's conjecture (위키백과), 2차 출처, 2026년 10월 30일 확인 ↩
19. Terence Tao on AI in mathematics (and beyond), a living summary (tao-web, 2026년 10월 28일 최종 업데이트), 2026년 10월 30일 확인 ↩