Executive Summary

2026년 10월 6일 밤, 오픈AI 가 깃허브에 openai/math 라는 저장소를 열었다. 안에는 공개되지 않은 내부 모델이 쓴 수학 원고 722편이 들어 있었다. 원고 하나가 결과 하나인 것은 아니고, 여러 편이 한 결과를 이루기도 해서 저장소는 그 묶음을 따로 세어 372개로 적는다. README 는 모델에게 던진 문제가 약 4,000개였고 결과 하나당 ChatGPT Pro 의 사고 연산을 평균 세 시간씩 썼다고 적는다. 4,000 과 722 사이에서 어느 결과가 어떤 기준으로 빠졌는지는 적혀 있지 않다. 저장소가 밝힌 것은 유의미한 수준을 갖춘 결과만 남기고 묶었다는 설명까지다.

같은 대목에 예외도 적혀 있다. README 는 결과의 대부분이 같은 절차로 나왔다고 적은 뒤, 그 절차를 따르지 않은 작업으로 둘을 이름 지어 든다. 리만 제타 함수의 영점 없는 영역에 관한 작업과 CM 아벨 다양체에 대한 호지 추측 증명이다. 그리고 앞의 작업 가운데 실수부 11/12 초과 영역을 다룬 원고는 읽기 쉽도록 사람이 손봤다고 덧붙인다. 공개 시점 판본과 현재 판본에서 이 세 문장은 똑같다. 다만 어느 원고가 어느 절차로 나왔는지를 원고별로 적은 기록은 따로 없다. 원고 디렉터리마다 들어 있는 README 는 이 글이 연 것들이 모두 같은 모양이었다. 제목과 저자와 날짜, 그리고 인용용 BibTeX 블록이다. 고친 원고에는 판본 메모가, 철회된 원고에는 철회 통지가 그 자리에 붙는다. 그리고 두 번째 예외로 이름이 불린 그 증명이 이 절 끝에서 다룰 032번 묶음의 머리 논문이다.

이 글은 그 저장소를 공개 시점 커밋과 현재 커밋으로 각각 내려받아, 파일 안의 목록을 직접 세어 쓴 것이다. 그러니 먼저 사흘 사이에 무슨 일이 있었는지부터 시간 순으로 적는다. 뒤에 나오는 모든 비율이 이 사흘 안에서 만들어졌다.

1.1한 사건에 날짜가 셋이다

보도는 대체로 "하루 만에 철회"라는 틀로 이 일을 전했다. 1차 문서를 열면 그 하루가 셋으로 갈린다. 철회 통지 본문은 스스로 10월 6일에 철회했다고 적고, 저장소의 변경 이력 파일은 그 작업을 10월 7일 항목 아래 적으며, 그 변경이 실제로 깃에 들어온 커밋 시각은 10월 8일 새벽이다. 어느 하나가 거짓이라기보다 문서마다 다른 시점을 적었다. 그래서 이 글은 날짜를 하나로 줄이지 않고 셋을 나란히 둔다.

커밋 두 건의 시각은 깃허브 API 로 직접 조회했다. 통지가 적은 철회일과 공개일이 같은 날이고, 깃에 반영된 것은 이틀 뒤다.

▲ 위 표의 네 자리를 시간축에 늘어놓은 것이다. 오른쪽 괄호가 표시한 구간은 통지가 적은 철회일과 그 변경이 실제로 깃에 들어온 시각 사이다.

1.2바뀐 것은 셋이 빠지고 스물일곱이 고쳐진 일이다

변경 이력 파일이 적는 작업은 셋이다. 원고 세 편을 철회했고, 열네 편을 고쳐 새 판본을 올렸고, 열세 편은 고쳐진 판본을 인용하도록 참고문헌만 손봤다. 뒤의 둘을 합치면 새 판본이 생긴 원고가 스물일곱 편이다. 이 글이 두 시점의 목차 파일을 디렉터리 단위로 맞대어 센 수도 스물일곱으로 같았다. 이 수가 5절에서 다시 나온다.

고쳐진 열네 편이 저장소 전체에 흩어져 있지는 않다. 변경 이력은 그것들을 주제별로 묶어 적는다. 립시츠 높이와 애슈킨–텔러 전류 쪽이 네 편, 쾰러 최소모형 프로그램과 풍부성 쪽이 여섯 편, 길들임과 초심플렉틱 변형 쪽이 두 편이고, 나머지 둘은 한 편씩이다. 앞의 세 묶음만 합쳐도 열두 편이라 수정은 세 주제에 몰려 있었다. 나머지 둘 가운데 하나는 증명을 고친 것도 아니다. 없어진 보조 원고를 가리키던 머리말의 낡은 인용 하나를 지운 것이다. 고친 내용으로는 증명 보수, 진술 교정, 가설과 의존 관계를 더 또렷하게 적은 것이 열거돼 있다.

원고 수는 722 에서 719 로 줄었는데 결과 묶음 수는 372 그대로다. 빠진 세 편이 한 묶음 안에 들어 있었기 때문이다.

1.3부호 하나가 세 편을 무너뜨렸다

철회 통지 세 건은 같은 뿌리를 가리킨다. 032번 묶음에 들어 있던 9월 18일자 원고 한 편에 부호를 잘못 매긴 자리가 있었고, 같은 묶음의 다른 두 편이 그 구성을 가져다 썼다. 세 편 모두 032번 한 묶음 안에 있었고, 그 묶음은 공개 시점에 원고 여덟 편을 담고 있었다. 지금은 다섯 편이다. 통지는 부호를 잘못 매긴 자리를 이렇게 적는다. 증명은 역-안정화 궤적마다 부호를 +1 로 매겨 전부 더하면 0 이 된다고 주장했는데, 두 가지의 방향이 서로 반대라서 이 관례에서는 궤적마다 부호가 −1 이어야 한다는 것이다.

"증명은 역-안정화 궤적마다 부호 +1 을 매긴다. … 이 관례에서는 각 역방향 궤적에 부호 −1 이 주어진다." 원문: "The proof assigns each reverse stabilization trace sign $+1$ … gives sign $-1$ for each reverse trace in this convention."

부호를 바로잡으면 더해서 0 이 되어야 할 값이 0 이 아니게 된다. 통지가 적는 결과값은 −2m 이고, m 은 0 보다 크다. 그 값이 0 이 아니면 증명이 기대고 있던 소거 정리의 전제가 깨진다. 수학적으로 더 들어가지 않아도 이 글에 필요한 것은 여기까지다. 한 편에서 부호 하나가 뒤집혔고, 그 한 편에 기대 있던 두 편이 함께 내려왔다.

통지에는 문장 하나가 더 있다. 세 건이 토씨 하나 다르지 않게 같은 문장으로 닫는다.

"이 철회는 증명에 관한 것이며, 해당 수학 명제가 거짓이라고 주장하는 것이 아니다." 원문: "This withdrawal concerns the proof; it does not assert that the mathematical statement is false."

정확한 문장이고, 이 글도 그 선을 지킨다. 증명이 무너졌다는 것과 명제가 거짓이라는 것은 다른 말이다. 수학에서 전자의 상태에 있는 명제는 다시 추측으로 돌아간다. 그리고 통지는 철회 전 원고를 가리키는 보관 주소에 저장소 커밋 해시를 그대로 박아 뒀다. 경로가 아니라 해시라서, 뒤에 파일이 어떻게 바뀌어도 그 시점의 PDF 는 같은 주소로 열린다. 이 글이 뒤에서 비어 있는 칸을 여럿 세지만, 이 칸은 잘 적힌 쪽이다.

1.4세 편이 빠지면서 묶음의 머리 주장도 좁아졌다

"세 편 철회"라는 표면 수치가 한 가지를 가린다. 목차 파일에서 032번 묶음의 제목이 바뀌었다. 공개 시점에 그 줄은 "모든 사영 K3 곡면에 대한 호지·쿠가–사토 결과"였고, 지금은 "CM 아벨 다양체에 대한 유리 호지 추측"이다. K3 곡면 전체를 대상으로 삼던 문장이 통째로 사라지고, 더 좁은 대상에 대한 문장이 그 자리에 들어왔다.

제목 아래 딸린 요약을 두 판본에서 맞대면 어느 문장이 빠졌는지가 보인다. 공개 시점 요약은 세 문장이었고, 첫 문장은 그때도 이미 CM 아벨 다양체를 대상으로 적고 있었다. K3 곡면 쪽은 마지막 문장이 맡았다. 딸림 결과들이 사영 복소 K3 곡면의 임의 곱에 대한 유리 호지 추측과 쿠가–사토 대응의 대수성을 보인다는 문장이다. 철회된 두 편이 바로 그 딸림 결과 둘이고, 지금 요약에는 그 마지막 문장이 없다. 그래서 묶음 제목이 요약 첫 문장과 같아졌다. 한 겹 더 있다. README 의 예외 대목은 공개 첫날부터 이 작업을 "CM 아벨 다양체에 대한 호지 추측 증명"이라 불렀고, 그 문장은 두 판본에서 한 글자도 다르지 않다. 즉 좁은 이름은 처음부터 저장소 안에 있었고, 목차가 그 이름으로 옮겨 온 것이다. 묶음의 머리 논문도 그 이름을 제목으로 단 원고로 바뀌었다.

수학 쪽 내용은 이 글의 범위 밖이다. 기록의 모양만 보면, 사라진 것은 원고 세 편이라기보다 한 부류 전체에 걸린 머리 주장이고, 그 변화는 원고 수 722→719 라는 수치에 아무 흔적도 남기지 않는다. 같은 저장소의 두 파일이 같은 묶음을 서로 다른 넓이로 부르고 있었다는 사실도 그 수치에는 남지 않는다.

지금 openai/math 의 README 를 열면 형식 검증을 얼마나 했는지가 한 줄로 적혀 있다. 저장소의 top-line 결과 가운데 약 42%가 형식화됐다는 문장이다. 이 한 줄이 보도에 가장 많이 인용된 수치의 출처다. 그런데 공개 시점 커밋에서 같은 자리를 열면 그 문장이 없다. 같은 불릿, 같은 위치에 다른 문장이 있다.

두 커밋에서 README 를 각각 내려받아 같은 불릿을 맞댄 것이다. 수치가 생긴 것만이 아니라 세는 대상이 바뀌었다.

이틀 사이에 두 가지가 바뀌었다. 낱말이 수치가 됐고, 세는 대상이 원고에서 top-line 결과로 옮겨 갔다. 뒤의 변화가 더 크다. 원고는 저장소가 파일로 세는 단위라서 누구나 똑같이 셀 수 있지만, top-line 결과는 그렇지 않다. 그 말이 무엇을 한 건으로 세는지는 다음 절에서 따로 본다.

그 한 줄만 바뀐 것도 아니다. 같은 커밋이 저장소의 설명 문서 세 곳을 같이 손봤다. 첫째, 바로 아래에 변경 이력 파일을 가리키는 줄이 새로 생겼고, 가리켜진 그 파일 자체가 이 커밋에서 처음 만들어졌다. 공개 당시에는 무엇이 언제 바뀌었는지 적는 자리가 저장소에 없었다는 뜻이다. 둘째, Lean 쪽 검증 도구 안내문이 늘었다. 공개 시점에는 설치와 실행 명령 열 줄이 전부였는데, 주 정리가 아니라 보조 결과를 검증하는 설정 다섯 가지를 이름으로 적은 절과, 논문별 적용 범위와 한계는 따로 있는 범위 설명 문서를 보라는 줄이 이때 붙었다. 셋째, 원고 수를 적은 줄이 722에서 719로 바뀌었다.

정리하면, 저장소가 자기 작업의 범위와 한계를 설명하는 문장들은 공개 이틀 뒤 한 커밋에 모여 들어왔고, 널리 인용된 42% 라는 수치도 그중 하나다. 그래서 이 글은 수를 셀 때마다 어느 커밋에서 센 값인지를 함께 적는다. 반대로 4절에서 볼 칸은 두 커밋에서 똑같다. 그 대목에서는 바뀌지 않았다는 사실 자체가 세어야 할 값이다.

먼저 쓰인 단위로 다시 재 보면 "많다"가 가리킨 값이 나온다. 공개 시점 형식화 목록에 오른 원고는 162편이고 전체 원고는 722편이니, 원고로 세면 22.4%다. 현재 커밋으로 다시 세도 23.9%다. 그러니 "많다"라는 낱말이 섰던 자리의 실제 값은 뒤에 적힌 42% 와 20%포인트 가까이 떨어져 있다.

저장소에는 형식화 카탈로그라는 파일이 하나 있다. 어느 논문을 Lean 으로 형식화했는지 적어 둔 목록이고, 파일 첫 줄 주석이 스스로 범위를 밝힌다. 주 결과가 형식화된 논문의 목록이라는 것이다. 이 목록을 세고, 목록이 가리키는 경로를 목차 파일과 맞대면 비율이 나온다. 저장소가 README 에 적은 비율과는 다른 값이다.

어느 쪽이 틀렸다는 뜻이 아니다. 셋은 서로 다른 것을 세고, 그 셋이 서기 전 같은 자리에 있던 것은 수치가 아니라 낱말이었다. 아래 도식이 그 넷을 한 자리에 모은 것이다.

네 자리가 서로 다른 것을 센다. 형식화 카탈로그와 경로가 이어진 논문, 그 논문이 속한 결과 묶음, 저장소가 README 에 적은 비율, 그리고 공개 당일 그 자리에 있던 낱말이다. 앞의 둘은 이 글이 저장소 파일을 직접 세어 얻은 값이고, 셋째는 저장소가 적은 값이며, 넷째는 수치가 아니다. 카탈로그의 논문 항목 자체는 173개인데 그중 172개만 현재 목차와 경로로 이어진다. 남은 한 건이 5절의 그 원고다.

3.1162 와 300 은 앞뒤가 아니다

널리 퍼진 이야기는 이렇다. 공개 때 162편이었는데 추가 작업으로 300편이 됐다는 것이다. 저장소 자신의 기록이 그 순서를 부정한다. 변경 이력 파일은 10월 7일 작업으로 형식화 여섯 건과 다른 추가 다섯 건을 더해 합계가 719편 중 300편이 됐다고 적는다. 여섯을 더해 300 이 됐다면 그 직전은 294 이지 162 가 아니다.

그럼 162 는 무엇인가. 공개 시점 형식화 카탈로그의 항목 수다. 이 글이 직접 세었고, 현재 판본에서는 173개다. 늘어난 열하나는 변경 이력이 적은 "형식화 여섯 + 다른 추가 다섯"과 정확히 맞는다. 즉 같은 작업이 한쪽 장부에서는 열하나로, 다른 쪽 장부에서는 여섯으로 적혔다. 두 수는 시점이 다른 것이 아니라 세는 규칙이 다르다.

3.2"top-line result" 는 저장소 어디에도 정의가 없다

42% 의 분모와 분자가 무엇을 세는지 알려면 그 말의 뜻이 필요하다. 이 글은 여덟 자리를 찾았다. README, 변경 이력, Lean 라이브러리 안내문, Comparator 안내문, 저장소가 함께 올린 개요 PDF 전문, 커밋 메시지 세 건, 저장소 코드 전체 검색, 그리고 이슈와 PR 목록. 그 말이 등장하는 자리는 README 의 그 한 문장과 변경 이력의 한 문장뿐이고, 둘 다 뜻을 적지 않는다. 개요 PDF 에서는 아예 한 번도 나오지 않는다. 이슈와 PR 은 둘 다 0건이라 외부가 물어볼 창구도 없었다.

정의가 없으니 분자를 역으로 맞춰 보는 수밖에 없다. 카탈로그 파일 안에는 셀 수 있는 목록이 여럿 있다. 전부 세어 봤고, 300 과 맞는 것은 없었다.

현재 커밋 기준이다. 분자 300 은 이 파일이 가진 어떤 목록의 길이와도 맞지 않는다. 저장소 바깥의 집계일 수도 있고 셈법이 다른 내부 장부일 수도 있지만, 공개된 파일로는 확인할 수 없다.

표의 둘째 줄은 이름까지 가깝다. 카탈로그 파일 안에는 main_results, 그러니까 주 결과라는 이름이 붙은 목록이 실제로 있고, 거기 오른 Lean 선언이 200개다. 공개 시점에는 185개였다. 주 결과를 기계가 읽을 수 있는 형식으로 열거한 자리는 저장소에서 이 목록뿐인데, 그 길이도 300 이 아니다.

더 눈에 띄는 것은 두 목록이 서로 이어져 있지 않다는 점이다. 같은 파일 안에 논문 173편과 선언 200개가 나란히 있는데, 어느 논문이 어느 선언으로 형식화됐는지를 적는 줄이 없다. 규격에는 그 자리가 둘이나 마련돼 있다. 원문 서술과 형식 선언을 맞대어 적는 칸이 하나, 논문마다 어느 정리나 어느 절을 가리키는지 적는 칸이 하나다. 두 칸 모두 이 파일에서 한 번도 쓰이지 않았다. 그러니 어느 논문의 어느 문장이 그 논문의 주 결과인지를 저장소 파일에서 읽어 낼 방법도 없다. 정의가 없는 것은 "top-line result" 라는 낱말만이 아니다.

3.3가장 많이 읽힌 해설이 300 의 출처로 건 파일에 300 이 없다

이 사건을 다룬 해설 가운데 가장 널리 읽힌 것은 멜리사 리가 The Conversation 에 쓰고 phys.org 가 받은 10월 9일 글이다. 그 글은 오픈AI 가 집필 시점까지 주 결과 300건을 형식화했다고 주장한다고 적고, 그 문장에 형식화 카탈로그 파일 링크를 건다. 이 글이 두 판본을 모두 받아 문자열을 검색했다. 그 파일에 "300"은 한 번도 나오지 않는다. 300 이 적힌 곳은 변경 이력 파일 한 곳뿐이다.

읽는 쪽의 잘못이라고 하기 어렵다. README 의 그 줄이 카탈로그 링크와 비율을 한 문장 안에 넣어 뒀기 때문이다. Lean 라이브러리와 형식화 카탈로그가 어떤 형식 증명이 있는지 설명한다고 적은 바로 다음에, 같은 문장 꼬리로 저장소의 약 42%가 형식화됐다고 적는다. 링크를 따라간 독자는 비율이 그 카탈로그에서 나온 값이라고 읽게 된다. 실제로 그 카탈로그를 세면 173이다.

3.4저장소 안에는 세 번째 기록이 따로 있다

카탈로그 말고도 형식화를 적어 둔 자리가 저장소 안에 하나 더 있다. lean/docs/ 아래 242개 파일인데, 결과 묶음마다 그 논문의 Lean 증명이 정확히 무엇을 보였는지 사람이 읽는 산문으로 적고 실재하는 Comparator 파일을 링크한다. 이 글이 전부 열어 링크된 논문 경로를 뽑았더니 340편이 나왔다. 그중 168편은 형식화 카탈로그에 없다. 표본으로 두 건을 직접 열어 보니 링크된 Lean 파일이 실제로 있었고 빈 껍데기도 아니었다.

이 문서들이 적는 내용은 범위다. 파일마다 어느 원고에 딸린 형식화인지 밝히고, Lean 증명이 무엇을 보였는지를 사람이 읽는 문장으로 적은 다음, 보이지 않은 것까지 적는 경우가 있다. 예를 들어 π 의 무리수 지수를 다룬 묶음의 범위 설명은, 논문이 따로 끌어낸 플린트힐스 급수 쪽 결론은 이번에 고른 명제 바깥이라고 못 박는다. 형식화가 원문의 어디까지 닿았는지를 적는 일을 이 문서들은 산문으로 하고 있다.

찾기 어려운 자리에 있지도 않다. 저장소의 목차 파일이 묶음마다 이 범위 설명으로 가는 링크를 달아 두는데, 공개 시점에 이미 235개였고 지금은 242개다. 앞 절에서 본 Comparator 안내문에도 논문별 적용 범위와 한계는 이 문서들을 보라는 줄이 있다. 다만 그 줄이 붙은 것은 공개 이틀 뒤다.

3.5이 수치는 이렇게 다시 셀 수 있다

이 절의 모든 수는 공개된 파일에서 나왔으니 누구나 다시 셀 수 있다. 공개 시점 커밋과 현재 커밋으로 형식화 카탈로그를 각각 내려받아 논문 항목을 세고, 그 항목이 가리키는 원고 디렉터리 경로를 목차 파일과 맞대면 된다. 제목으로 맞대면 안 된다. 같은 논문인데 한쪽은 유니코드 기호를 쓰고 다른 쪽은 ASCII 로 풀어 적은 쌍이 다섯 있고, 아예 제목이 똑같은 서로 다른 논문도 한 쌍 있다. 이 저장소에서 논문을 세는 유일하게 안정적인 단위는 파일 경로다.

공개 시점 커밋은 adc7f124, 현재 커밋은 fd4aeeb2 다. 이 글을 쓰는 2026년 10월 13일까지 그 뒤로 추가 커밋은 없었다.

여기서 낱말 하나를 먼저 갈라야 한다. 이 사건을 다루는 글에서 "검증"은 적어도 세 가지 다른 일을 가리킨다. 섞어 쓰면 아래 문단이 전부 틀리게 읽힌다.

셋은 서로를 대신하지 못한다. 3절에서 센 비율은 전부 첫째에 관한 것이고, 이 절이 보는 것은 둘째다.

기계 검사가 둘째를 대신하지 못한다는 것 자체는 이 글이 처음 하는 말이 아니다. 페블러스도 2026년 8월 9일 리포트에서 형식 검증이 닫지 못하는 자리를 다섯 패턴으로 정리해 뒀다. 이 글은 그 설명을 되풀이하지 않는다. 이번에 새로 생긴 것은 따로 있다. 그 공백이 한 벤더의 기계 판독 메타데이터에 등급으로 적혀 있다는 것이다.

4.1목록 파일 맨 끝에 적힌 값

3절에서 센 그 카탈로그 파일의 맨 끝에는 목록이 아니라 이 작업 전체를 설명하는 블록이 있다. 내용은 세 줄이다.

공개 시점 커밋과 현재 커밋에서 이 블록은 한 글자도 다르지 않다.

이 파일 형식은 오픈AI 가 만든 것이 아니다. mathlib-initiative 가 관리하는 공개 규격이고, openai/math 는 그 0.4 버전을 쓴다. 규격 문서를 직접 받아 보면 review.status 칸의 설명문에 권장 어휘가 여섯 단으로 적혀 있다. 검토 안 함, 에이전트 검토, 자기 평가, 동료 검토, 저자 확인, 그 밖의 자유 기술 순이다. 저장소가 적은 값은 그 여섯 가운데 맨 아래다.

▲ 저장소가 실제로 적은 값(강조)과 설명문이 적어 둔 나머지 다섯 값이다. 순서는 본문이 인용한 설명문 그대로이며, 이 칸 자체는 강제되는 열거형이 아니다.

이 여섯 단은 규격이 강제하는 값 목록이 아니다. 규격 파일에서 이 칸의 타입은 그냥 문자열이고, 여섯 단은 설명문에 적힌 권장 관례다. 바로 옆의 automation.method 칸은 다섯 값을 실제로 강제하는데, review.status 는 그렇지 않다. 그러니 "표준이 정한 6단계의 맨 아래"가 아니라 "표준이 권장 어휘로 여섯 단을 제시해 둔 자유 기술 칸에 맨 아래 값이 적혀 있다"가 정확한 서술이다.

다만 블록 자체는 비워 둘 수 있는 자리가 아니다. 규격이 반드시 있어야 한다고 못 박은 최상위 칸은 넷인데, 프로젝트 정보와 출처 목록과 자동화 방법, 그리고 이 검토 블록이다. 저장소가 고른 것은 적을지 말지가 아니라, 적어야 하는 칸에 무엇을 적을지였다. 고른 값이 맨 아래 값이다. 다음 절에서 볼 칸들은 사정이 반대다. 그쪽은 비워 둬도 규격이 아무 말도 하지 않는 자리다.

같은 블록의 다른 칸들도 함께 봐야 한다. 누가 검토했는지 적는 칸과 어떻게 검토했는지 적는 칸은 비어 있고, 형식화를 만든 방법으로는 에이전트가 적혀 있다. 묶으면, 기계가 만든 형식 증명을 사람이 원래 주장과 대조했는지에 대해 저장소는 기계가 읽는 자리에 "안 했다"고 적어 둔 셈이다.

4.2비어 있는 것은 이 칸 하나가 아니다

규격 전문을 읽고 openai/math 의 카탈로그에서 선택 칸을 하나씩 찾아봤다. 쓰인 것이 없다. 형식화가 원문과 벌어지는 지점을 적는 칸, 원문 서술과 형식 선언을 맞대어 적는 칸, 원저자가 형식화에 참여하거나 승인했는지 적는 칸, 증명 안에 비워 둔 자리가 몇 개인지와 어떤 공리를 썼는지 적는 칸, 증명이 가정한 미증명 외부 결과를 적는 칸, 어떤 모델과 도구로 얼마를 들여 자동화했는지 적는 칸이 모두 그렇다. 여섯 갈래로 묶어 적었지만 규격에서는 칸이 더 잘게 갈린다. 비워 둔 자리를 세는 칸이 둘이고 쓴 공리를 적는 칸이 따로 있으며, 자동화 쪽도 모델과 도구와 비용이 각각이다. 칸으로 세면 열 종이다.

선택 칸을 통째로 안 썼다는 말은 아니다. 쓰인 것도 있다. 작업 범위를 "부분적 진척"이라는 한 줄로 적은 칸이 그렇고, 3절에서 센 선언 200개 목록이 그렇고, 가져다 쓴 Lean 라이브러리를 열거한 칸도 그렇다. 갈리는 지점은 다른 데 있다. 쓰인 쪽은 무엇을 했는지 적는 칸이고, 비어 있는 쪽은 그것이 원문을 얼마나 덮었는지와 누가 그것을 확인했는지 적는 칸이다. 위에 꼽은 열 종이 모두 뒤쪽이다.

이것도 한쪽으로 읽지 않는다. 비워 둔 칸이 추적을 안 했다는 뜻인지, 추적은 했는데 적지 않은 것인지는 공개된 파일로 알 수 없다. 쓸 수 있는 데까지만 쓰면 이렇다. 규격이 제공하는 선택적 투명성 칸 열 종 가운데 채워진 것이 없다.

4.3같은 주에 수학자가 적은 문장이 그 칸을 겨눈다

10월 9일, 테렌스 타오의 블로그에 Lean 정리 증명기에 관한 초대 기고가 실렸다. 글쓴이는 타오가 아니라 수학자 토머스 헤일스다. Lean 을 어떻게 다뤄야 하는지에 대한 일반론이고, 그 안에 이 글의 칸을 그대로 가리키는 문장이 있다.

"Lean 으로 쓰인 증명은, 명제가 원문에 충실한지 확인하는 사람의 감사가 이루어지기 전에는 받아들여서는 안 된다." 원문: "a proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity."

같은 글에서 그는 이 말을 더 쉬운 두 물음으로 푼다. 검증된 정리가 우리가 생각하는 바로 그것인가. Lean 안의 정의들이 우리가 생각하는 그 정의에 대응하는가. 그가 형식 검증을 깎아내리는 것이 아니라는 점도 같이 적어 둬야 공정하다. 그는 같은 글에서 Lean 증명은 커널이 확인하기 전까지는 믿어서는 안 된다고도 적는다. 기계 검사를 반드시 하라는 쪽이고, 그다음 문장 대조를 더 하라는 쪽이다.

범위를 분명히 해 둔다. 이 기고에서 헤일스가 든 오픈AI 사례는 9월 8일 나비에–스토크스 발표이지 10월 6일의 722편 공개가 아니다. 그는 이번 공개를 논평하지 않았다. 이 글이 두 문장을 나란히 놓는 것은 다른 이유에서다. 수학자는 사람의 감사 전에는 받아들이지 말라고 적었고, 저장소는 바로 그 감사를 적는 칸에 "안 함"이라 적었다. 날짜가 사흘 차이일 뿐 서로를 보고 쓴 글이 아니다.

4.4그 공백을 같은 날 arXiv 논문이 수학 문제로 다뤘다

저장소가 공개된 바로 그날, arXiv 에 논문 한 편이 제출됐다. 킹스칼리지런던과 케임브리지의 바스투니스·치르첼리·한센이 쓴 것이고, 제목부터 번역에서 잃어버린다는 말을 쓴다. 주장은 이렇다. 수학 자연어 문장의 모호성을 푸는 문제는 가해성 복잡도 지수에서 임의로 높은 자리에 있고, 그 지수가 무한이다. 정지 문제의 지수가 1 이니, 뜻에 충실한 자동 형식화는 정지 문제를 포함한 어떤 계산 문제보다도 어렵다는 말이 된다.

추상적 걱정으로만 남지 않았다. 논문은 오픈AI 의 나비에–스토크스 Lean 형식화에서 자연어 서술과 형식 명제가 어긋난 자리 두 곳을 짚는다. 한 곳은 미분 횟수로, 자연어 쪽 부등식이 요구하는 매끄러움보다 Lean 쪽이 한 단계 더 센 조건을 건다. 다른 한 곳은 압력과 플럭스의 한계를 다루는 식인데, Lean 쪽 부등식에 자연어 서술에는 없는 변수가 하나 들어가 있다.

저자들이 단 유보를 반드시 함께 읽어야 한다.

"유의: 우리는 오픈AI 의 자연어 증명이 옳은지에 대해 아무 주장도 하지 않는다. 우리가 말하는 것은 Lean 으로의 오역에 관한 것뿐이다." 원문: "Disclaimer: We do not make claims about the correctness of OpenAI's NL proof, we only make statements about mistranslations into Lean."

이 논문의 범위도 좁다. 들여다본 것은 9월 8일의 형식화 한 건이지 722편이 아니다. 722편의 Lean 형식화에서 불일치가 발견됐다고 쓰면 거짓이다. 쓸 수 있는 문장은 이것이다. 형식 명제와 자연어 명제가 어긋날 수 있다는 것은 추상적 걱정이 아니고, 같은 회사의 다른 Lean 산출물에서 두 자리가 실제로 어긋난 채 발견됐으며, 그 보고가 이 저장소가 공개된 바로 그날 제출됐다.

한 줄로 줄이면, 기계는 번역문이 말이 되는지는 검사한다. 그 번역문이 원문과 같은 말인지는 검사하지 않는다. 그 일을 사람이 했는지 적는 자리가 review 칸이고, 거기 적힌 값이 "안 함"이다.

1절에서 센 수로 돌아간다. 새 판본이 생긴 원고는 스물일곱 편이었다. 그 스물일곱을 공개 시점 형식화 카탈로그와 맞대면 한쪽으로 쏠린다. 스물여섯 편은 카탈로그 바깥에 있었고, 안쪽에 있던 것은 한 편이다. 철회된 세 편도 셋 다 바깥이었다.

이 쏠림을 어느 쪽으로도 단정하지 않는다. 형식화가 오류를 걸러 냈다고 읽을 수도 있고, 형식화되지 않은 쪽만 사람이 들여다봤기 때문이라고 읽을 수도 있다. 저장소는 어느 쪽인지 적지 않았다. 이 글이 적을 수 있는 것은 고친 자리가 목록의 경계를 거의 그대로 따라갔다는 사실까지다. 그보다 중요한 것은 경계 안쪽의 한 편이다.

5.1안쪽 한 편에서 판본이 어긋났다

네 다양체 위의 길들임이 양립성을 함의한다는 제목의 원고다. 10월 6일에 새 판본이 생기면서 디렉터리 이름의 날짜가 9월 23일에서 10월 6일로 바뀌었다. 새 판본의 README 에는 판본 메모가 붙었는데, 그 메모가 적은 변화 가운데 하나가 조건을 좁힌 것이다. 원뿔 합 등식이 성립하는 범위를 특정 조건으로 제한했다는 문장이다. 다만 목차 파일의 한 줄 요약에는 이 좁힘이 나오지 않는다. 거기에는 무엇을 추가했는지만 적혀 있고, 범위를 좁힌 대목은 디렉터리 안 README 의 판본 메모에만 있다.

그런데 형식화 카탈로그의 그 항목은 공개 시점과 지금이 완전히 같다. 가리키는 경로가 여전히 9월 23일 디렉터리다. 3.4절에서 본 세 번째 기록도 마찬가지다. 이 묶음의 범위 설명 문서 역시 두 커밋에서 한 바이트도 다르지 않고, 본문에 링크한 PDF 가 9월 23일 판본이다. 즉 Lean 쪽 기록은 둘인데 둘 다 옛 판본을 가리킨다. 그리고 그 9월 23일 디렉터리 README 를 열어 보면 대체됐다는 표시가 없다.

주장이 좁혀진 원고와, 그 원고를 형식화했다고 적힌 기록 둘이 서로 다른 판본을 가리킨다. 목차 파일은 새 판본을 가리키도록 갱신됐고, Lean 쪽 기록 둘은 갱신되지 않았다.

한 가지가 더 있다. 옛 판본 디렉터리의 README 에는 그 판본을 인용하라고 내준 BibTeX 블록이 그대로 들어 있다. 새 판본 README 는 판본 메모에서 옛 판본을 링크해 거슬러 올라갈 길을 열어 두는데, 반대 방향은 열려 있지 않다. 옛 판본 쪽에서는 더 새로운 판본이 있다는 사실을 알 길이 없고, 인용 블록은 아무 표시 없이 인용을 받을 준비가 된 채로 남아 있다.

그래서 그 Lean 증명이 틀렸다는 뜻인가. 알 수 없다. 좁힌 쪽이 더 약한 주장이니 형식화가 여전히 성립할 수도 있고, 형식 명제가 지금은 없어진 넓은 주장을 가리키고 있을 수도 있다. 둘이 맞는지는 아무도 확인하지 않았다. 같은 파일이 그 자리에 "안 함"이라 적고 있기 때문이다.

5.2이 경우를 적는 칸이 규격에 따로 있다

4절에서 지나간 선택 칸 가운데 하나가 정확히 이 상황을 위한 자리다. 규격에는 fidelity.divergences 라는 칸이 있고, 설명문이 무엇을 적으라는지까지 밝혀 둔다. 형식화가 원문에서 벌어지는 지점, 즉 일반화한 곳, 가정을 약화한 곳, 보조정리 이름을 바꾼 곳이다. 가정을 약화했다는 말이 이 원고에서 벌어진 일과 같은 종류다. 그런데 openai/math 의 카탈로그에는 이 칸이 비어 있는 정도가 아니라 fidelity 블록 자체가 없다. 두 판본 모두 그렇다.

나란히 놓고 보면 저장소가 잘한 쪽도 같이 보인다. README 는 고친 원고의 옛 판본을 계속 열람 가능하게 두겠다고 적었고, 실제로 그렇게 해 뒀다. 1절에서 본 철회 통지의 커밋 해시 고정도 같은 성격이다. 판본을 보존하는 일은 이 저장소가 제대로 한 쪽에 속한다. 비어 있는 것은 보존이 아니라 대조다. 어느 판본이 어느 형식 증명과 짝인지를 적는 자리, 그리고 둘이 어긋난다면 어떻게 어긋나는지를 적는 자리다. 둘 다 비었다.

그 약속이 원고 바깥까지 미치지는 않는다. 저장소가 함께 올린 개요 PDF 가 그렇다. 컬렉션 전체를 설명하는 문서이고, 수정 커밋에서 내용이 바뀌었다. 표지에 적힌 원고 수가 722 에서 719 로 줄었다. 그런데 표지 날짜는 10월 6일 그대로이고, 판본 메모도 새 파일 이름도 없다. 옛 판본은 깃 이력을 거슬러 올라가야 나온다. README 가 한 약속은 원고를 두고 한 말이니 이것을 약속 위반이라 부를 일은 아니다. 다만 이 글이 세는 것은 약속이 아니라 칸이다. 같은 날짜를 단 문서 두 개가 서로 다른 수를 적고 있는데, 둘을 구분할 표시가 문서 안에 없다.

저장소가 열리기 일주일 전인 9월 29일, 수학·AI 자문단이 「AI 가 생성한 수학의 책임 있는 공개」라는 문서를 냈다. 600건이 넘는 설문 응답을 근거로 삼았고, 번호 붙은 권고 다섯을 담았다. 이 문서를 읽기 전에 자문단이 어떻게 생겼는지부터 적어 두는 편이 공정하다.

발족 공지에 따르면 출발점은 오픈AI 쪽이었다. 오픈AI 가 몇몇 수학자에게 외부 자문위원회를 만들자고 먼저 접촉했고, 접촉받은 쪽이 그 대신 독립 기구를 만들어 다른 사람들을 초청하기로 했다. 호스트는 프린스턴 고등연구소다. 구성은 아홉 명이다. 프랑수아 샤를, 카밀로 데 렐리스, 티모시 가워스, 마틴 헤어러, 니킬 스리바스타바, 울리케 틸만, 라비 바킬, 에드워드 위튼, 멜라니 매쳇 우드가 이름을 올렸다. 일부 요약이 테렌스 타오를 이 자문단 일원으로 적는데, 아홉 명 명단에 그의 이름은 없다. 그는 발족 공지를 자기 블로그에 실었을 뿐이다. 그러니 이 권고는 바깥에서 날아온 비난이 아니라, 오픈AI 가 부른 자리에서 독립 기구로 바뀌어 나온 문서다.

6.1세 번째 권고가 요구한 다섯 가지

다섯 권고 가운데 이 글과 맞물리는 것은 세 번째다. 결과를 공개할 때 무엇을 함께 공개하라는 조항이고, 항목이 다섯이다.

"공개하는 결과마다 AI 연구소는 모델의 이름, 쓴 프롬프트, 요약된 사고 과정, 걸린 시간, 추정 연산 비용을 공개해야 한다." 원문: "For each result released, the AI lab should make public the name of the model, the prompts used, a (summarized) chain of thought, the time taken, and the estimated cost of computation."

이 다섯을 저장소가 실제로 공개한 것과 맞대 보면 한 칸이 드러난다. 다섯 가운데 넷은 4절에서 본 그 파일 형식에 적어 넣을 전용 칸이 이미 있다. 모델 가중치를 공개하라는 요구가 아니라, 이름과 프롬프트와 시간과 비용을 적으라는 요구이기 때문이다.

권고 전문과 형식화 카탈로그, 그리고 그 카탈로그가 따르는 규격 0.4 버전을 각각 열어 맞댄 것이다. 권고는 다섯을 결과마다 공개하라고 적었고, 저장소가 이행한 것은 하나를 총평으로, 하나를 열 묶음에 대해서다.

권고 하나가 더 겹친다. 다섯 번째는 문제의 해답을 낼 때마다 AI 가 정확히 어떻게 쓰였는지를 분명히 기록하라고 적는다. 저장소가 그 일을 한 자리는 1절에서 본 README 의 세 문장이다. 결과 대부분이 같은 절차로 나왔고, 그 절차를 따르지 않은 작업이 둘 있으며, 그중 한 원고는 사람이 읽기 쉽도록 손봤다는 서술이다. 컬렉션 전체를 두고 한 말이라는 점에서 권고가 요구한 단위와 어긋난다. 1절에서 본 대로 원고 쪽 README 에는 그런 서술이 들어갈 자리가 없다. 다만 그 세 문장이 예외를 이름까지 들어 밝힌다는 점은 적어 둘 만하다. 균일한 공정이었다고 뭉뚱그리지 않은 쪽이다.

6.2같은 규격을 쓴 다른 프로젝트는 그 칸을 채웠다

비어 있는 칸을 두고 물을 수 있는 반문이 있다. 원래 다들 비워 두는 칸 아닌가. 규격을 만든 조직의 저장소 목록을 열어 같은 형식을 쓴 프로젝트를 찾아봤다. 실수합 추측이 실수에서 거짓임을 보인 형식화 프로젝트가 그 칸들을 실제로 채워 뒀다. 검토 상태에는 자기 평가와 에이전트 감사라고 적고, 검토자 이름과 검토 메모를 달고, 쓴 모델과 도구와 걸린 기간과 비용까지 적는다. 독립 동료 검토가 아니라는 한계도 스스로 적어 놨다.

이 사례 하나로 일반화하지 않는다. 그 프로젝트는 정리 한 건에 저자 넷인 소규모이고 openai/math 와는 크기가 다르며, 쓰는 규격 버전도 0.3 으로 한 단계 앞이다. 그러니 다른 프로젝트는 대체로 채운다는 말은 할 수 없다. 할 수 있는 말은 이것이다. 적어도 한 곳은, 같은 생태계 안에서, 같은 칸을 사람이 읽을 수 있게 채웠다.

6.3공개한 쪽의 칸도 고르지 않다

다섯 가운데 부분적으로 이행된 한 칸, 즉 사고 과정 요약을 공개한 열 묶음을 따로 봤다. 이 열 묶음을 먼저 적은 것은 TechCrunch 다. 이 글이 더하는 것은 그 열 묶음과 형식화 카탈로그가 거의 겹치지 않는다는 점이다. 열 묶음에 속한 논문은 스물두 편이고 그중 카탈로그에 오른 것은 아홉 편이다. 묶음 단위로 보면 열 중 여섯은 카탈로그 기준으로 형식화가 하나도 없다.

이 문장에는 단서가 붙는다. 3.4절에서 본 세 번째 기록을 다시 맞대면, 그 여섯 묶음 전부가 lean/docs/ 에는 범위 설명과 실재하는 Comparator 파일을 갖고 있다. 그러니 형식화가 하나도 없다는 말은 공식 카탈로그를 기준으로 할 때만 참이다. 두 기록이 서로 다른 답을 준다는 사실이 여기서 한 번 더 나온다. 덧붙이면 그 여섯 묶음의 목차 항목에는 범위 설명으로 가는 링크가 공개 첫날부터 달려 있었다. 읽으려는 사람에게서 감춰진 것은 없었고, 집계에 들어가지 않았을 뿐이다.

6.4권고를 낸 쪽이 이행 판정을 거부했다

같은 주에 수학 쪽에서 나온 목소리가 둘 더 있다. 둘 다 이 글의 주제와는 다른 이야기라 자리만 적어 둔다. 하나는 10월 6일 18시경 테렌스 타오가 마스토돈에 올린 네 편짜리 글이다. 공개 문제의 해답이 지속 가능하지 않은 방식으로 대규모 수확되고 있고, 그 결과 수학의 여러 분야가 전통적 방식으로 풀리던 때보다 훨씬 척박해진다는 내용이다. 두 가지를 분명히 해야 한다. 이 글은 저장소 공개보다 약 네 시간 빠르고, 글 안에 오픈AI 라는 이름이 나오지 않는다. 이 공개를 보고 쓴 글도, 특정 회사를 지목한 글도 아니다. 다른 하나는 10월 7일에 나온 인간 수학 학회의 성명이다. 회원 808명 명의이고, 700개가 넘는 파일을 한꺼번에 내놓는 것은 학술의 시연이 아니라 힘의 시연이라고 적었다. 이 글은 그 입장을 지지하지도 반박하지도 않는다.

정작 권고를 낸 자문단은 10월 6일 성명에서 두 걸음 물러섰다. 먼저 자신들의 자문 역할이 이 결과들의 영향에 대한 판단이나 오픈AI 가 그 결과를 얻은 과정에 대한 승인으로 해석되어서는 안 된다고 적었다. 그리고 이렇게 닫는다.

"우리는 오픈AI 와 그것들을 논의했고 회사가 대화에 응한 점을 높이 산다. 그 논의가 건설적이었다고 보지만, 우리 권고가 어느 정도까지 제대로 따라졌는지를 평가하는 일은 결국 수학 공동체의 몫이다." 원문: "We have discussed them with OpenAI and appreciate the company's willingness to engage. While we consider these discussions constructive, it is ultimately up to the mathematical community to assess the extent to which our recommendations were followed successfully."

권고를 쓴 쪽이 따랐는지는 자기가 판정하지 않겠다고 적었으니, 이 글도 판정하지 않는다. 이 글이 한 일은 다섯 항목과 네 개의 빈 칸을 나란히 놓는 것까지다. 그 정도로도 충분히 또렷하다. 덧붙이면, 권고의 여는 요청은 비공개 모델에서 고급 수학 문제를 시험하는 일을 멈춰 달라는 것이었고 openai/math 의 README 첫 문단은 모델 개발의 일환으로 공개 연구 문제에서 모델을 평가한다고 적는다. 이 충돌은 TechCrunch 가 먼저 적었다.

페블러스 관심의 이유

페블러스가 파는 것이 바로 그 칸이다

페블러스가 하는 일은 데이터가 AI 에 쓸 만한 상태인지 판정하고, 그 판정을 뒤에 읽을 수 있는 기록으로 남기는 일이다. 이번 사건이 보여 주는 것은 그 일이 세상에서 검증 문화가 가장 엄격한 분야에서조차 제대로 돌아가지 않는다는 점이다. 핵심은 양이 아니다. 722편을 한꺼번에 올린 것이 문제가 아니라, 무엇이 어떤 등급으로 확인됐는지 적는 칸을 아무도 채우지 않았다는 것이다. 그리고 6절이 보여 주듯 그 칸은 이미 있었다. 칸을 만드는 일, 채우는 일, 채워진 칸을 읽는 일은 서로 다른 일이고, 이 사건에서 제대로 갖춰진 것은 첫 번째뿐이다.

검증에는 층이 셋 있고 대부분 첫째만 센다

4절에서 가른 세 가지는 수학에만 있는 구분이 아니다. AI 가 만든 학습 데이터와 합성 데이터와 라벨에도 똑같은 세 층이 있다. 스키마 검사를 통과한 것, 사람이 원본과 대조한 것, 그 분야가 쓸 만하다고 인정한 것이다. 대부분의 조직은 첫째만 세고 그 수를 "검증된 데이터"라고 부른다. 둘째를 센 조직은 드물고, 셋째를 기록으로 남긴 조직은 더 드물다.

5절의 판본 어긋남이 그 위에 한 겹을 더한다. 판본이 어긋나는 순간 첫째 층의 기록조차 무엇에 대한 검사인지 알 수 없어진다. 페블러스가 2026년 8월 리포트에서 AI 증명의 계보가 남지 않는다고 적었던 바로 그 지점인데, 이번에는 계보가 남았고 대신 어긋났다. 기록을 남기는 일과 그 기록이 가리키는 대상을 맞추는 일은 서로 다른 일이다.

▲ 페블러스 원본 도식. 4절에서 오픈AI 저장소를 두고 가른 기계 검사·문장 대조·수학계 평가의 구분을, AI 산출물 일반(학습 데이터·합성 데이터·라벨)으로 넓힌 이 글의 해석이다.

조직에 대 볼 네 가지 질문

첫째, "검증됐다"의 등급을 적는 칸이 우리 산출물 기록에 있는가. 없다면 비율부터 세지 말고 어휘부터 정해야 한다. 검토 안 함과 에이전트가 본 것과 사람이 표본으로 본 것과 전수로 대조한 것은 같은 낱말로 불릴 일이 아니다. 둘째, 그 칸을 읽는 사람이 있는가. 이번 사건에서 오픈AI 는 그 칸을 채웠다. 가장 낮은 값으로, 기계가 읽는 자리에, 공개 첫날부터 적어 뒀다. 아무도 읽지 않았을 뿐이다.

셋째, 검증 기록이 가리키는 판본과 지금 쓰이는 판본이 같은가. 커밋이나 해시로 못박혀 있는가, 아니면 디렉터리 경로로만 걸려 있는가. 경로는 이름이 바뀌면 조용히 빗나가고, 빗나간 뒤에도 파일은 멀쩡히 열린다. 넷째, 우리가 적는 "검증 통과율"의 분모가 무엇인가. 건수인가, 묶음인가, 주 결과인가. 한 조직 안에서 세 수가 동시에 유통되고 있지는 않은가. 3절에서 본 것이 정확히 그 상태다.

같은 자를 우리에게 댄다

페블러스가 서는 자리는 AI 산출물의 검증 등급을 적는 칸을 표준으로 만들고, 그 칸이 채워졌는지를 세는 쪽이다. 생성량 경쟁에는 참여하지 않는다. 거기에는 이미 참가자가 충분히 많다. 그리고 같은 자를 우리에게 먼저 대면 빈 칸이 나온다. 페블러스의 DataClinic 리포트와 합성 데이터 산출물에는 review.status 에 해당하는 칸이 아직 정식으로 없다. 이 글이 오픈AI 의 빈 칸을 세는 글이니, 우리 쪽 빈 칸을 먼저 적어 두는 것이 순서다.

참고문헌

이 글의 대상 — 저장소 파일

• 1.OpenAI, openai/math — 공개 시점 커밋 adc7f124(2026-10-06 21:58:50Z), 수정 커밋 30148886(2026-10-08 05:03:50Z), 현재 커밋 fd4aeeb2(2026-10-08 05:20:00Z). 이 글의 모든 수치는 앞뒤 두 판본의 README.md·CONTENTS.md·history.md·lean/formalization.yaml 을 각각 내려받아 센 것이다. 2절의 안내문 비교와 5절의 판본 대조는 같은 두 커밋의 lean/ComparatorChallenges/README.md·overview.pdf·lean/docs/342.md 와 해당 원고 디렉터리의 README 두 개를 추가로 받아 맞댄 것이다.
• 2.철회 통지 세 건 — preprints/<디렉터리>/README.md. 셋 다 "Withdrawn on October 6, 2026." 으로 시작하고 같은 문장으로 닫는다. 부호 오류 수식이 적힌 것은 9월 18일자 「Algebraicity of Weil classes on split abelian eightfolds」 통지이고, 보관 커밋 해시는 세 건 모두에 박혀 있다.
• 3.lean/docs/ 242개 파일과 lean/ComparatorChallenges/README.md · 저장소가 함께 올린 overview.pdf — 3.2절의 용어 탐색과 3.4절의 세 번째 기록이 여기서 나왔다. lean/docs/ 로 가는 길은 둘이다. CONTENTS.md 가 묶음마다 거는 링크(공개 시점 235개, 현재 242개)와 Comparator 안내문의 "per-paper coverage and limitations" 줄이다. ⚠️ 뒤의 줄은 수정 커밋에서 붙었고, lean/README.md 자체는 이 디렉터리를 설명하지 않는다.
• 4.OpenAI, Sharing AI progress in mathematics — ⚠️ 공식 발표문. 이 글을 쓰는 동안 접근이 막혀 전문을 읽지 못했다. 본문에서 발표문의 내용을 인용하지 않은 이유다.

규격과 권고

• 5.mathlib-initiative, formalization.yaml 규격 0.4 버전 — review.status 의 권장 어휘 여섯 단, automation.method 의 강제 값 다섯, 그리고 4.2절이 센 선택 칸 열 종이 여기 정의돼 있다.
• 6.mathlib-initiative, sum_product 의 formalization.yaml — 6.2절의 대조 사례. ⚠️ 규격 0.3 버전을 쓰고 정리 한 건짜리 소규모 프로젝트다. 이 한 건으로 생태계 일반화를 하지 않았다.
• 7.AGMAI(Advisory Group on Mathematics and Artificial Intelligence), Responsible Release of AI-Generated Mathematics, 2026-09-29 — 600건이 넘는 설문 응답을 근거로 삼았고 번호 붙은 권고는 다섯이다. 6.1절의 축자는 세 번째 권고에서 가져왔다.
• 8.AGMAI, Statement on OpenAI's Release of Mathematical Results, 2026-10-06 — 6.4절을 닫는 축자의 출처. 자문단이 이행 평가를 수학 공동체의 몫으로 넘긴 문장이다.
• 9.자문단 발족 공지, 2026-09-21 — 아홉 명 명단과 오픈AI 가 먼저 접촉한 경위가 여기 적혀 있다. ⚠️ 테렌스 타오는 이 공지를 자기 블로그에 실었을 뿐 아홉 명 명단에 없다.

학술·전문가

• 10.Thomas Hales, What mathematicians should know about the Lean Theorem Prover(타오 블로그 초대 기고), 2026-10-09 — ⚠️ 글쓴이는 테렌스 타오가 아니라 토머스 헤일스다. 이 기고가 든 오픈AI 사례는 9월 8일 나비에–스토크스 발표이고 10월 6일 공개가 아니다.
• 11.A. Bastounis · F. Circelli · A. C. Hansen, Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs, arXiv:2610.08144, 2026-10-06 제출 — 4.4절의 두 불일치와 저자 유보의 출처. ⚠️ 이 논문이 본 것은 나비에–스토크스 형식화 한 건이다.
• 12.Terence Tao, Mathstodon 스레드 네 편, 2026-10-06 18:00Z — ⚠️ 저장소 공개보다 약 네 시간 빠르고 오픈AI 를 지목하지 않는다.
• 13.Association for Human Mathematics, AHM Statement on OpenAI's October 6 Release, 2026-10-07, 회원 808명 — ⚠️ 이 성명은 타오 블로그에도 전재됐지만 타오의 말이 아니다.

보도와 해설

• 14.Melissa Lee(The Conversation), phys.org 전재, 2026-10-09 — 3.3절의 대상. 300 의 출처로 형식화 카탈로그를 링크했는데 그 파일에 300 은 없다.
• 15.TechCrunch(팀 펀홀츠), 2026-10-08 — 권고의 여는 요청과 README 첫 문단의 충돌, 사고 과정 요약 열 묶음, 멜라니 매쳇 우드 인용을 먼저 적은 보도다. 6.3절과 6.4절의 귀속이 여기로 간다. · aiweekly.co, 2026-10-09 — 162 라는 수가 유통된 경로.

페블러스 블로그 인접 글

• 16.AI 수학 증명의 계보 공백(2026-08-09) — 이 글의 직계 선행편. 형식 검증이 닫지 못하는 자리를 다섯 패턴으로 정리한 절이 4절의 출발점이다. · 필즈상 수상자들의 선언(2026-09-14) · 라이덴 선언(2026-06-30).