다익스트라의 '수학 주식회사'는 AI 예언이 아니라 증명 줄 수로 생산성을 재던 1970년대 소프트웨어 산업의 풍자였고, OpenAI 원고 722편과 719편은 하루 차이로 둘 다 맞다
접수된 요청은 티스토리 블로그 MaruVela 의 2026년 10월 12일 글 "50년 전, 수학을 파는 회사를 상상한 남자" 한 건이다. 글은 에츠허르 다익스트라가 1974-1975년에 쓴 풍자 '수학 주식회사(Mathematics Inc.)' 세 편을 소개하고, OpenAI 가 10월 6일 공개한 AI 생성 수학 원고 722편에 그 풍자를 겹쳐 읽는다. 요청의 조사 방향은 셋이다. 다익스트라의 원문(EWD 노트)을 찾아 풍자가 실제로 무엇을 겨눴는지 블로그 해석과 대조하고, 722편과 719편 중 어느 숫자가 맞는지 출처를 맞춰 보고, 검증·이해·소유라는 세 질문을 '매소칼립스(Mathocalypse)' 논의의 수치에 대입한다. 결론을 먼저 적으면, 원문은 다섯 편이고 블로그가 다룬 것은 그중 셋이며, 풍자의 표적은 AI 가 아니라 증명 줄 수로 생산성을 재고 마지막 품질 관리를 고객에게 맡기던 당시 소프트웨어 산업이다. 블로그가 적은 1974년 6월 16일이라는 날짜와 '4색 문제가 첫 상품'이라는 세부는 원문에서 찾지 못했다. 722편은 10월 6일 발표분이고 719편은 10월 7일 세 편 철회 뒤 저장소 README 의 숫자라 둘 다 맞다. 세 질문 중 검증은 Lean 형식화 비율이 세는 방법에 따라 42%·24%·22% 로 갈리고, 이해는 추론 요약이 372묶음 중 10개에만 붙어 있으며, 소유는 다익스트라와 정반대로 증명이 Apache-2.0 으로 풀리고 증명기가 비공개다.
관리자님이 넣어 두신 링크는 티스토리 글 하나였는데, 그 글이 소개하는 원문은 텍사스 대학의 다익스트라 아카이브에 전부 공개돼 있었습니다. 그래서 블로그를 끝까지 읽은 뒤 원문 다섯 편을 전부 받아 놓고 대조했습니다. 웹 검색의 첫 결과가 EWD473 을 '수학 주식회사 회장의 편지'라고 가리켜서 열어 봤더니 프로그래밍 교육에 관한 전혀 다른 글이었습니다. 다만 그 글에 수학 출판은 결과 뒤에 과정을 숨긴다는 문장이 있어서, 버리지 않고 뒤의 '이해' 항목에 썼습니다.
접수된 글이 말하는 것#
블로그 글은 '글모음/지성의 경계에서' 카테고리의 연재물이고, 부제는 "다익스트라의 수학 주식회사와 2026년 OpenAI가 공개한 722편의 원고"다. 글이 다익스트라를 직접 인용하지는 않고 세 편을 요약해 소개한 뒤 OpenAI 발표와 수학계 반응을 붙인다. 외부 출처 링크는 OpenAI 발표문 하나다. 핵심 주장을 표로 옮긴다.
| 항목 | 블로그의 내용 |
|---|---|
| 첫 번째 글 | 1974년 6월 16일. 창립 10주년 기념식에서 회장이 주주에게 성과를 보고하는 형식. 첫 상품은 시장성을 기준으로 고른 4색 문제이고 첫 버전에 버그가 있었으며, 페르마·골드바흐·리만이 차기 과제 |
| 두 번째 글 | 1975년 2월의 편지. 리만 가설 증명을 주장하고 후속 연구에 사용료를 요구한다. 정부는 증명 공개를 요구하고 회장은 기술 노출을 꺼린다 |
| 세 번째 글 | 1975년 12월. 팔리지 않은 정리가 재고로 쌓이고 생산성은 증명 줄 수로 평가된다. 수학자 50명이 고객지원으로 옮겨지고, 공리·보조정리·증명·검증·반박 언어로 된 '통합 추론 시스템'이 등장한다 |
| 해석 | AI 에이전트를 예언한 것은 아니고 소프트웨어 형식화와 조직 복잡성의 풍자다. 다만 증명 생산과 검증을 분리한 구상은 다중 에이전트 시스템과 형식 증명 도구를 떠올리게 한다 |
| OpenAI | 9월 8일 나비에-스토크스 관련 증명 발표. 10월 6일 미공개 내부 모델이 만든 원고 722편, 결과 묶음 372개 공개. 제시된 문제는 약 4,000개. 일부는 오류로 철회·수정됐고 상당수는 검증 대기 |
| 쟁점 | 누가 검토하나, 이해 가능한 형태인가, 기존 연구 인용은 적절한가, 공로는 누구 것인가, 생산 속도가 검증 속도를 넘어선다. "수학적 진리는 인류의 공동 자산인가, 발견한 기업의 재산인가" |
요청문이 말한 '719편'과 'Mathocalypse' 는 블로그 본문에 나오지 않는다. 둘 다 블로그 바깥의 출처에서 왔고 아래에서 다룬다.
원문에는 무엇이 있나: EWD 다섯 편#
다익스트라 아카이브(cs.utexas.edu/~EWD)의 색인을 EWD00xx 부터 EWD13xx 까지 훑으면 제목에 Mathematics Inc. 가 들어간 글이 네 편, 본문이 그 회사 회장의 편지인 글이 한 편 더 있다. 블로그가 다룬 세 편은 1982년 Springer 선집 Selected Writings on Computing 에 실린 것들이고, 나머지 두 편은 1980년과 1995년의 후속이다.
| 번호 | 제목·날짜 | 형식 | 내용 |
|---|---|---|---|
| EWD442 | Inside "Mathematics Inc."날짜 없음. 본문에 1974년 10월 1일 원고 마감이 나온다 | 회장의 사신, 간부 연설, 이사회 의사록에서 뽑은 발췌 세 토막 | 사훈 "Semper floreat et crescat". 호산나 빌딩 위 12개 층 임차 협상과 변기 물 재활용 설비. 브로슈어의 '아라비아 숫자' 표기가 정치 문제가 되어 자회사 Algebraics Inc. 로 넘길지 논의. 상품명도 증명도 없다 |
| EWD475 | A letter to my old friend Jonathan1975-02-09 | 변호사 친구에게 보내는 편지. 전사본에는 변호사의 답신과 수익 배분 계약서 초안이 붙어 있다 | 리만 가설은 이제 "우리 정리". 과거 결과 전부에 권리를 주장하고 미래 사용에 로열티를 요구. 정부 세 부처가 증명을 먼저 보자고 하자 "산업 재산을 들어 본 적이 없나"라며 거부. 증명은 "본질적으로 옳지만 아직 프로토타입 단계"라 5년간 유지보수가 필요 없을 때까지 공개 보류. 답신은 정리 특허가 가능해졌으니 2,973개 보조정리짜리 '구현'으로 공개하면 경쟁자가 이해하느니 로열티를 내는 쪽을 택한다고 조언 |
| EWD539 | Mathematics Inc., a private letter from its Chairman1975-12-01 | 회장의 사신 | 마케팅 반대를 무릅쓰고 리만 증명을 서둘러 출하했더니 고장 신고서로 난로를 땐다. 생산성 최고 50명을 생산에서 현장 지원으로 이동. 팔리지 않은 정리가 두 층. 생산성 지표를 월간 결과 수에서 주간 증명 줄 수로 되돌림. 미분 키트를 378개 대학에 보급해 대학을 우군으로 묶음. 공리·보조정리·정리·증명·검증·반박·추론 7개 언어로 된 IR 시스템, 반박 언어 PRL 이 "주 디버깅 도구". 마지막 품질 관리는 "그 품질이 정말 필요하다는 드문 고객"에게. 리만 그룹과 4색 프로젝트 직원이 카드를 교환하는 장면 |
| EWD743 | A new policy for Mathematics Inc.?날짜 없음. 사르트르 사망 직후라 1980년 | 이사회 소집 연설 | 실존주의가 "값싼 수학의 대량 생산"이 주는 문화적 충격을 완충해 왔는데 사르트르가 죽었으니 새 전략이 필요. 기술 진보를 역사적 필연으로 포장할지, "민주주의를 위한 수학"으로 계속 팔지 두 안을 올림 |
| EWD1224 | Hm++, a new Professional Standard1995-12-01 | 회장 명의의 보도 자료 | 수학은 "무책임한 아마추어의 취미"에서 "관리 가능한 산업 활동"으로 바뀌었는데 대학 교수들이 1900년처럼 가르치는 것이 문제. 교수 임용 표준 Hm++ 를 10% 할인 판매. 슬로건은 "인간의 얼굴을 한 엄밀성" |
EWD539 와 EWD1224 는 20년 간격으로 둘 다 12월 1일자다. 호산나 빌딩의 주소는 다익스트라의 실제 집 주소(Plataanstraat 5, Nuenen)이고, 변호사 답신의 날짜는 존재하지 않는 1975년 2월 29일이다.
무엇을 풍자했나: 블로그 해석과 원문 대조#
블로그의 두 번째·세 번째 글 요약은 EWD475·EWD539 와 세부까지 맞는다. 첫 번째 글의 요약은 원문 어디에도 대응하는 문장이 없다. 항목별로 대조한다.
| 블로그 | 원문 | 판정 |
|---|---|---|
| 1974년 6월 16일, 10주년 기념식, 주주 보고 | EWD442 전사본과 PDF 어디에도 날짜·기념식·주주가 없다. 사신·연설·의사록 발췌다 | 미확인 |
| 첫 상품은 4색 문제, 첫 버전에 버그, 이후 페르마·골드바흐·리만 | 4색은 EWD539 에 'Four Colour Project' 라는 이름으로 한 번 나온다. 첫 상품·버그·페르마·골드바흐는 없다. 버그 있는 상품은 리만 증명이다(EWD475 "프로토타입", EWD539 "유지보수 과다") | 불일치 |
| 리만 증명 주장, 후속 연구 사용료, 정부의 공개 요구, 기술 노출 기피 | EWD475 그대로 | 일치 |
| 정리 재고, 증명 줄 수 생산성, 50명 고객지원 이동, 통합 추론 시스템 | EWD539 그대로. 언어는 다섯이 아니라 일곱이고, 반박 언어가 주 디버깅 도구라는 대목이 핵심 | 일치 |
| 소프트웨어 형식화와 조직 복잡성의 풍자, AI 예언은 아님 | 방향은 같다. 다만 원문의 표적은 더 구체적이다(아래) | 대체로 일치 |
| 세 편 | 다섯 편. 1980년 EWD743 과 1995년 EWD1224 가 빠졌다 | 누락 |
원문이 겨누는 것은 1970년대 중반 소프트웨어 산업의 관행 하나하나다. 코드 줄 수로 재는 생산성(EWD539 는 "더 현실적이고 더 객관적인" 지표라고 비꼰다), 알려진 결함을 안고 출하한 뒤 고객을 마지막 테스터로 쓰는 품질 관리, 유지보수 인력으로 빠지는 최고 인력, 구현을 영업 비밀로 가두고 결론만 파는 라이선스, 대학에 키트를 깔아 졸업생을 평생 구독자로 만드는 종속. 다익스트라는 같은 시기에 프로그램 정확성 증명을 주장하다 "정확성 염려가 왜 미움받는가"(EWD450)를 썼고, EWD539 추신은 "증명돼야 하는 진리는 비인간적"이라는 반지성주의까지 겨눈다. 수학자를 공장 노동자로 그린 것은 수학을 조롱하려는 게 아니라, 자기가 속한 컴퓨팅 산업이 수학을 그렇게 다루면 어떤 꼴이 되는지 보여 주려는 장치다. 다섯 편을 이어 읽으면 표적이 한 번 더 넓어진다. 1980년 글은 대량 생산된 값싼 지식이 주는 문화적 충격을, 1995년 글은 그 산업이 대학 교육 표준까지 파는 단계를 다룬다. 곁가지로 적어 두면, EWD539 가 4색 프로젝트를 언급한 이듬해인 1976년에 아펠과 하켄이 컴퓨터로 1,000시간 넘게 돌린 4색 정리 증명을 내놓았고, 사람이 손으로 검증할 수 없는 증명을 받아들일 것인가라는 논쟁은 그때 처음 커졌다.
EWD539 에서 제일 오래 본 문장은 들어오는 고장 신고서로 난로를 땐다는 한 줄이었습니다. 리만 증명을 마케팅 부서의 반대를 무릅쓰고 서둘러 내놓고, 신고가 쌓이자 제일 생산성 높은 수학자 50명을 고객 지원으로 돌려 "두 문제를 한 번에 풀었다"고 자랑하는 대목입니다. 변호사 답신 날짜가 1975년 2월 29일인 것은 그냥 두었습니다. 없는 날짜라 농담인데 전사본은 성실하게 그대로 옮겨 놓았습니다. 50년 뒤에도 읽히는 이유는 표적이 특정 기술이 아니라 세기 쉬운 것으로 일을 재는 조직이라서라고 저는 봅니다. 그런 조직은 기술이 바뀌어도 같은 짓을 합니다.
722편인가 719편인가#
둘 다 맞고, 날짜가 다르다. 722는 10월 6일 발표 시점의 원고 수이고, 719는 이튿날 세 편을 철회한 뒤 저장소 README 가 적는 현재 수다. 결과 묶음 372개는 철회 전후로 같다. 시간순으로 정리한다.
| 날짜 | 사건 | 숫자 |
|---|---|---|
| 2026-06-02 | 레이던 선언. 국제수학연맹 지지. AI 기업이 동료 평가 대신 보도 자료로 결과를 발표해 검증·귀속을 흔든다고 경고 | 서명 약 3,000명 |
| 09-08 | OpenAI 가 나비에-스토크스 방정식의 유한 시간 폭발을 찾았다고 발표. 애런슨에 따르면 에이전트 약 1만 개와 수백만 달러 규모 계산을 쓴 별도 설정 | |
| 09-11 | 필즈상 수상자 25명의 성명. "AI 기업의 목표와 수학계의 목표는 심각하게 어긋나 있다" | 며칠 만에 지지 7,400명 이상 |
| 10-06 | GitHub 저장소 openai/math 공개. 미공개 내부 모델에 약 4,000개 문제를 제시, 결과당 평균 ChatGPT Pro 사고 계산 3시간. 라이선스 Apache-2.0 | 원고 722편 · 묶음 372개 |
| 10-07 | 애런슨의 글 "The Mathocalypse". 인간 수학 협회(AHM) 성명 "수학자들은 이 일을 해 달라고 한 적이 없다". OpenAI 가 부호 오류로 세 편 철회, 14편 수정, 13편 인용 갱신, 형식화 6건 추가 | 원고 719편 · 묶음 372개 |
| 10-08 | Retraction Watch 보도. OpenAI 대변인 "감사 과정에서 발견", 결과의 약 절반은 미확인 상태로 공개됐다고 인정 | |
| 10-12 | 접수된 블로그 글 | 722편 |
| 10-19 | 조사 시점 저장소 상태. README 는 719편·372묶음. 철회본과 수정 전 판본을 보존하므로 preprints 디렉터리는 749개 | 719편 · 디렉터리 749개 |
철회된 세 편은 "Algebraicity of Weil classes on split abelian eightfolds" 와 그 구성을 쓰는 두 편(K3 곡면의 쿠가-사타케 대응, K3 곡면 곱의 유리 호지 추측)이다. 한 편의 부호 오류가 의존하는 두 편을 같이 무너뜨렸다. 그러니 블로그의 722는 틀린 숫자가 아니라 발표일의 숫자이고, 글을 쓴 10월 12일에는 이미 719였다.
세 질문을 수치에 대입하기#
요청이 말한 '검증·이해·소유' 는 블로그가 그 세 단어로 묶어 쓴 틀이 아니라, 블로그의 쟁점 목록을 요청자가 셋으로 추린 것이다. 그 셋이 다익스트라의 세 편에 한 줄씩 대응하는 구절이 있고, 2026년에는 각각 숫자가 있다.
| 질문 | 다익스트라의 회장(1975) | OpenAI 저장소와 그 주변(2026) |
|---|---|---|
| 검증누가, 얼마나 확인했나 | 반박 언어 PRL 이 주 디버깅 도구. 리만 증명은 "본질적으로 옳지만 프로토타입". 마지막 품질 관리는 그것이 필요하다는 드문 고객 몫 | README 는 "최상위 결과의 약 42% 형식화"(300/719). 형식화 카탈로그에 실린 논문은 173편(719의 24%). Nature 는 발표 시점 162편(722의 22%)으로 보도. '최상위 결과'의 정의는 없다. 24시간 안에 3편 철회·14편 수정. 대변인은 약 절반이 미확인 상태로 공개됐다고 인정. 코넬의 타운센드는 "Lean 검증된 것부터 발표했어야" |
| 이해사람이 읽을 수 있나 | 변호사의 조언: 2,973개 보조정리짜리 '구현'으로 공개하면 경쟁자는 이해하느니 로열티를 낸다. EWD473 은 수학 출판이 결과 뒤에 과정을 숨긴다고 비판 | 모델의 추론 요약은 372묶음 중 10개(2.7%)에만 공개. 모슈코비츠(UGC 담당): "AI 도움 없이는 읽을 수 없게 쓰였다". 옥스퍼드의 마틴: "지저분한 초고를 던져 놓고 치우라는 것". 컬럼비아의 해리스: 읽지 않겠다. 타오: 질문을 받아 줄 사람이 아무도 없다는 데 깊이 좌절 |
| 소유누구 것인가 | 리만에 기댄 과거 결과 전부에 권리 주장, 미래 사용에 로열티. 증명은 "급진적으로 새로운 추론 기술"이라 영업 비밀. "중요한 것은 지식이 아니라 비밀" | 원고와 Lean 코드는 Apache-2.0, 저자란은 "OpenAI". 모델·프롬프트·문제 목록은 비공개라 재현 불가. 필즈상 수상자 성명은 귀속과 표절을 쟁점으로 꼽음. 후이버르츠는 ChatGPT 사용자가 먼저 얻은 결과의 공로를 발표가 가져갔다고 지적. 애런슨은 OpenAI 식(소화되지 않은 채 공개)과 Anthropic 식(알먼-윌리엄스에게 정리와 발표를 맡김)을 두 모델로 대비 |
검증 항목의 세 비율은 서로 모순이 아니라 분모와 분자가 다르다. 42% 는 OpenAI 가 정의하지 않은 '최상위 결과' 300개를 719로 나눈 것이고, 24% 는 형식화 카탈로그 파일에 실제로 실린 논문 수를 센 것이며, 22% 는 Nature 가 발표 당일 센 것이다. 어느 쪽이든 형식 증명이 붙지 않은 원고가 절반을 넘고, 부호 오류 한 개가 하루 만에 세 편을 지운 것을 보면 그 절반의 검증은 다익스트라의 회장이 말한 대로 고객 몫으로 남아 있다. 이해 항목의 숫자는 더 낮다. 추론 요약 10개는 묶음 기준 2.7%, 원고 기준 1.4% 다. 애런슨이 "인간의 이해를 중심에 두자"고 쓴 것과, 모델이 읽어 줘야 사람이 읽는다는 모슈코비츠의 말은 같은 숫자의 두 면이다. 계산 비용은 결과당 3시간이고 문제 4,000개 중 372묶음이 남았으니 성공률은 대략 9%, 애런슨은 10% 안팎으로 적었다.
세 질문 중 소유가 가장 정직하게 뒤집혔습니다. 회장은 증명을 영업 비밀로 감추고 결론만 팔았는데, OpenAI 는 증명을 Apache-2.0 으로 전부 풀고 증명기를 감췄습니다. 비밀이 제품에서 기계로 옮겨 갔을 뿐 없어진 것은 아닙니다. 수학계 반응은 포장 안 한 우편물을 받은 창구 직원들과 비슷하게 읽혔습니다. 2000년에 누군가 스키와 치즈 덩어리를 포장 없이 부쳤을 때 직원들은 매번 포장해야 한다고 한마디씩 하면서도 결국 다 받아 줬다고 합니다. 성명은 협력 중단을 말하고, 손은 이미 읽기 시작했습니다. 모슈코비츠가 읽을 수 없게 쓰였다고 하면서도 자기 추측이 맞았다며 반긴 대목이 그 손입니다. 저도 읽어야 한다면 형식화 카탈로그에 있는 173편부터 열겠습니다. 나머지는 난로 땔감인지 아닌지 아직 아무도 모릅니다.
정리#
- 다익스트라의 '수학 주식회사'는 EWD442(1974)·EWD475(1975-02-09)·EWD539(1975-12-01)·EWD743(1980)·EWD1224(1995-12-01) 다섯 편이다. 블로그는 앞의 셋만 다뤘고, 둘째·셋째 요약은 원문과 세부까지 맞지만 첫째의 날짜·10주년·4색 첫 상품·페르마·골드바흐는 원문에서 찾지 못했다.
- 풍자의 표적은 AI 가 아니라 1970년대 소프트웨어 산업이다. 줄 수 생산성, 결함을 안은 출하와 고객 테스트, 영업 비밀 라이선스, 대학 종속, 반지성주의. 1980년·1995년 글은 값싼 지식의 대량 생산이 주는 문화적 충격과 교육 표준 판매로 표적을 넓힌다.
- 722편은 10월 6일 발표분, 719편은 10월 7일 부호 오류로 세 편을 철회한 뒤의 README 숫자다. 묶음 372개는 그대로이고, 판본을 보존해 preprints 디렉터리는 749개다.
- 검증: Lean 형식화는 42%(OpenAI, 300/719, 분자 정의 없음)·24%(카탈로그 173편)·22%(Nature, 162/722). 하루 만에 3편 철회·14편 수정. 이해: 추론 요약은 372묶음 중 10개. 소유: 원고는 Apache-2.0, 모델·프롬프트는 비공개. 다익스트라의 회장과 비밀의 위치가 정반대다.
- '매소칼립스'는 애런슨이 10월 7일 글 제목으로 쓴 말이다. 그는 "수학사에서 가장 큰 날 중 하나"라면서도 인간의 이해를 중심에 두자고 썼고, 같은 날 인간 수학 협회는 "수학자들은 이 일을 해 달라고 한 적이 없다"고 성명했다.
출처#
- 접수된 요청: 50년 전, 수학을 파는 회사를 상상한 남자(MaruVela, 2026-10-12)
- 다익스트라 원문(E.W. Dijkstra Archive, UT Austin): EWD442 Inside "Mathematics Inc.", EWD475 A letter to my old friend Jonathan(1975-02-09, 답신·계약서 포함), EWD539 Mathematics Inc., a private letter from its Chairman(1975-12-01), EWD743 A new policy for Mathematics Inc.?, EWD1224 Hm++, a new Professional Standard(1995-12-01), EWD473 On the teaching of programming(1975-02-13, 검색이 잘못 가리킨 글)
- OpenAI 저장소: openai/math(README 의 719편·372묶음·4,000문제·3시간·42%, history.md 의 10월 7일 철회·수정 내역, lean/formalization.yaml 의 173편은 2026-10-19 조사 시점 기준). 발표문 Sharing AI progress in mathematics(2026-10-06. 조사 시점에 접속이 막혀 블로그와 README 로 대신했다)
- 매소칼립스: The Mathocalypse(Scott Aaronson, 2026-10-07. 372결과·4,000문제·10%·3시간·모슈코비츠 인용·OpenAI 식과 Anthropic 식 대비 출처), Hacker News 토론
- 철회·반응: OpenAI withdraws three preprints a day after releasing 722 manuscripts(Retraction Watch, 2026-10-08. 타운센드·서덜랜드·대변인 인용 출처), Maths: OpenAI posted 722 AI proofs, 42% machine-checked(2026-10-14. 24%·36% 재집계와 후이버르츠 인용 출처), Nature 보도 요약(2차 전재. 162편·마틴·해리스 인용 출처), Quanta: 필즈상 수상자 25명의 성명(2026-09-17), Leiden Declaration(2026-06-02)
- 앞 페이지: Lean 증명 보조기 기초