Executive Summary

2026년 7월 19일 일요일, 하버드의 수학자 르반트 알푀게가 X에 짧은 글을 올렸다. “hello there the jacobian conjecture is false thanx.” 인사말과 오타 섞인 감사 인사 사이에 세 변수 다항식 사상 하나가 붙어 있었다. 그것으로 끝이었다. 1939년 이후 수학자들이 87년 동안 참이라고 믿어 온 야코비안 추측은 그 게시물 하나로 거짓이 됐다.

추측이 무엇을 주장했는지는 수학 없이도 말할 수 있다. 존 D. 쿡이 이 사건을 정리하며 붙인 글 제목이 정확히 그 진술이다. 국소적으로 어디서나 되돌릴 수 있다고 해서 전역적으로 되돌릴 수 있는 것은 아니다. 다항식으로 정의된 사상이 있고, 그 사상을 아주 좁은 영역에서만 보면 어느 지점에서나 되돌릴 수 있다고 하자. 야코비안 행렬식이 0이 아닌 상수라는 조건이 그 뜻이다. 야코비안 추측은 이 국소적 성질이 전역적 성질로 올라간다고, 그러니까 사상 전체가 일대일이라고 주장했다. 좁게 보면 어디서나 접히지 않는데 넓게 보면 겹칠 수 있는가. 87년 동안 아무도 겹치는 예를 찾지 못했다.

이번 반례는 그 겹침을 세 점으로 보여준다. 복소 3차원 공간에서 자기 자신으로 가는 7차 다항식 사상 F가 있고, 그 야코비안 행렬식은 상수 −2다. 조건은 완벽히 충족된다. 그런데 서로 다른 세 점 (0, 0, −1/4), (1, −3/2, 13/2), (−1, 3/2, 13/2)이 모두 같은 점 (−1/4, 0, 0)으로 간다. 일대일이 아니다. 테렌스 타오는 자기 블로그에서 이 사상을 그대로 재구성하며 “0이 아닌 상수 야코비안을 가지면서도 가역이 아닌 사상 F : ℂ³ → ℂ³가 존재한다”고 정리했다.

반례 하나면 추측은 거짓으로 확정된다. 다만 무엇이 거짓이 됐는지는 정확히 말해야 한다. 이번 반례는 3차원에서 구성됐고 같은 방식으로 3보다 높은 차원까지 자동으로 확장된다. 그러나 2차원 평면의 경우는 여전히 열려 있다. 타오도 “2차원에서 추측은 미해결로 남아 있고, 1차원에서는 쉽게 증명된다”고 못 박았다. 평면에서는 차수 100까지의 다항식에 대해 계산으로 반례가 없음이 확인된 상태다. “야코비안 추측이 무너졌다”는 요약은 절반만 맞다.

이 문제의 이력을 보면 87년이라는 숫자가 왜 무거운지 알 수 있다. 1884년 루트비히 크라우스가 2차원 특수 사례를 다뤘고, 1939년 오트하인리히 켈러가 지금 통용되는 형태로 일반화했다. 1998년 스티븐 스메일은 21세기 수학이 풀어야 할 문제 목록을 만들며 이것을 16번에 올렸다. 그 사이 세그레와 그뢰브너를 비롯해 여러 수학자가 증명을 발표했다가 미묘한 오류로 철회했고, 그렇게 무너진 논문이 최소 다섯 편이다. 훗날 소수 간격 문제로 이름을 알린 장이탕이 이 추측을 박사논문 주제로 삼았다가 결과를 논문으로 내지 못했다는 이력도 이 문제의 악명을 말해 준다. 이 반례가 다른 미해결 문제인 딕시미에 추측까지 함께 반증한다는 이야기도 나왔으나, 이는 2차 보도를 통해 전해지는 내용이고 타오의 글에는 언급이 없다.

이 사건에서 가장 많이 회자된 것은 속도다. 일요일 오후에 올라온 게시물을 수학자들이 그날 안에 독립적으로 확인했고, 런던의 케빈 버자드는 다음 날 아침 일어나 보니 이미 Lean으로 기계 검증이 끝나 있었다고 포춘에 말했다. 87년을 버틴 문제가 하루 만에 정리된 셈이다. 이 속도를 두고 “AI 시대에는 검증도 이렇게 빨라진다”는 해석이 뒤따랐다. 그 해석은 인과를 거꾸로 잡은 것이다.

빨랐던 이유는 반례의 형태에 있다. 반례를 확인하는 일은 세 점을 다항식에 대입해 같은 값이 나오는지 보고, 야코비안 행렬식을 전개해 상수 −2가 맞는지 보는 것이 전부다. 유한하고, 정확하고, 기호계산 도구를 쓸 줄 아는 사람이면 누구나 재현할 수 있다. 검증 비용이 거의 0에 가까웠다. 반례는 원래 그런 물건이다. 참을 증명하려면 모든 경우를 덮어야 하지만, 거짓을 보이려면 하나만 내밀면 된다. 이번에 AI가 만든 산출물은 검증하기 가장 쉬운 종류의 수학적 대상이었다.

그러니 이 사건은 검증 체계가 준비됐다는 증거로 읽으면 안 된다. 운이 좋았다는 증거로 읽는 편이 정확하다. 같은 시기에 같은 도구를 쓴 다른 작업들은 얼마나 걸렸을까.

여기서 갈리는 것이 검증 비용의 비대칭이다. AI는 산출 비용을 급격히 낮췄지만 검증 비용은 산출물의 종류가 결정하고, 그 종류는 우리가 고를 수 없다. 반례처럼 검증이 공짜인 결과가 나오면 하루 만에 합의가 서고, 긴 논증이 나오면 사람이 몇 달을 읽어야 한다. 야코비안 사건은 앞쪽 극단에 있었을 뿐이다. 덧붙이자면 이 결과도 아직 동료심사를 통과한 논문으로 출판되지는 않았다. 미해결 문제 추적 사이트에서 이 항목이 여전히 심사 대기 상태로 표시돼 있다는 이야기가 타오의 블로그 댓글을 통해 전해진다. 독립 확인과 동료심사 완료는 다른 단계다.

두 달 전에도 비슷한 장면이 있었다. 5월에 한 모델이 에르되시의 단위거리 추측을 반증했을 때, 수학자 아홉 명이 붙어 검증한 것은 모델의 원본 추론이 아니라 사람이 정리해 편집한 논증이었다. 그 사건은 페블러스가 별도의 글로 다뤘고, 6월의 라이덴 선언은 학습 단계의 동의와 귀속을 요구했다는 점에서 또 다른 글의 주제였다. 사흘 전 글에서는 LLM이 관찰을 새 이론으로 바꾸는 귀추적 도약을 못 한다는 진단을 다뤘다. 그쪽이 발견이란 무엇인가를 묻는 인식론의 문제라면, 이 글은 이미 만들어진 결과를 무엇으로 믿느냐는 인프라의 문제를 다룬다.

야코비안 반례에서 공개된 것은 반례 그 자체였다. 다항식 사상의 계수와 겹치는 세 점. 검증에 필요한 것은 전부 거기 있었다. 공개되지 않은 것은 그 계수가 어디서 왔는가에 관한 모든 것이다. 어떤 프롬프트를 넣었는지, 몇 번을 시도했는지, 모델이 헛다리를 짚었을 때 사람이 어디서 방향을 틀었는지, 어떤 버전의 모델이었는지. 학계 필자들이 쓴 해설 매체 더 컨버세이션은 이 상태를 그대로 적었다. “이 글을 쓰는 시점까지, 알푀게가 정확히 어떻게 모델에 프롬프트를 넣었고 모델의 출력이 어떤 모습이었는지에 관한 세부는 공개되지 않았다.”

공백은 회사 쪽에서도 그대로였다. 이 결과에 대한 공식 발표나 기술 블로그, 모델 카드 언급은 확인되지 않는다. 발표 자체가 회사 릴리스를 거치지 않은 개인의 소셜미디어 게시물이었고, 그 게시물은 2천만 회 넘게 읽혔다. 알푀게는 포춘의 취재 요청에 응하지 않았다. 심지어 공로를 어떻게 적을 것인가부터 정해진 것이 없었다. 타오의 블로그 댓글에서는 “모델이 풀었다”가 아니라 “르반트 알푀게가, 모델과 함께”가 정확한 귀속이라는 정정이 나왔다. 귀속 규범이 아직 없다는 사실이 사건 당일의 댓글에서 드러난 셈이다.

여기까지만 보면 결론은 쉽다. 회사가 더 많이 공개하면 된다. 그런데 2주 뒤 정확히 그 실험이 벌어졌다. 8월 3일 OpenAI는 미공개 모델 Astra가 미해결 문제 열 개를 풀었다고 발표하면서, 이번에는 Lean으로 작성된 형식 증명을 저장소에 올리고 모델의 사고 과정을 서술한 내러티브와 사람이 정리한 원고까지 함께 내놓았다. 야코비안 때와는 비교할 수 없이 많은 자료였다. 그런데 그중 한 문제를 냈던 헨리 유엔의 반응은 이랬다. “그게 나에게 어떤 이해도 주지 않는다. 그건 그냥 시간이 걸리는 일이겠지.” 원고가 기술적으로 흥미로운 대목을 오히려 묻어 버렸고, 왜 그런 접근을 택했는지가 설명되지 않는다는 것이 그의 지적이었다.

열 문제는 고차원 구 채우기, 콘의 강직성 추측, 에르하르트 부피 추측, 다색 램지 수, 양자 병렬 반복처럼 분야가 제각각인 미해결 문제였다. 증명은 공개 저장소에 Lean 코드로 올라갔고, 회사 쪽 연구자는 해답을 찾는 데 든 토큰이 자사 요율로 2천 달러쯤이라고 밝혔다. 결과와 형식 증명과 비용까지 나온 셈이다. 그런데도 문제를 낸 사람은 자기 문제가 왜 그런 경로로 풀렸는지 알지 못한다.

두 사건에서 닫힌 것과 남은 것은 이렇게 갈린다.

비교 조건이 없다는 지적도 나왔다. 게리 마커스는 “Astra 문제의 절반은 Fable로도 풀린다. OpenAI는 대조군조차 두지 않았다”고 했고, 실제로 야코비안 반례를 찾아낸 그 알푀게가 열 문제 중 다섯 개를 다른 모델로 24시간 안에 독립적으로 풀었다. 인터넷 접속 없이 일반적인 프롬프트만 썼다고 그는 밝혔다. 무엇이 이 모델의 고유한 능력이었는지 판별할 근거가, 발표 자료 안에는 없었다는 뜻이다. 재러드 두커 리히트만처럼 “수학사상 가장 중요한 날” 같은 규정에 제동을 건 목소리가 나온 것도 같은 맥락이다.

존 D. 쿡은 반례가 나온 직후 모델에게 직접 물었다. 반례가 나오기 전에 수학자들은 이 추측이 참이라고 믿었느냐고. 답은 이랬다. “질문의 전제가 정확하지 않습니다. 야코비안 추측에 대한 반례는 발견되지 않았습니다. 그것은 여전히 수학의 미해결 문제입니다.” 이건 학습 데이터 컷오프의 당연한 결과이고, 모델이 거짓말을 한 것이 아니다. 쿡 본인도 이 도구를 분필이나 화이트보드에 가까운 것으로 규정했다. 다만 상징으로는 정확하다. 산출에 관여한 주체조차 그 사건의 기록을 갖고 있지 않다.

이건 누가 무엇을 숨겼다는 이야기가 아니다. 알푀게도, 어느 회사도 규칙을 어기지 않았다. 기록을 남기라는 규칙이 아직 없기 때문이다. Astra 사례가 그 증거다. 성실하게 공개한 쪽에서도 같은 공백이 남았다면, 문제는 개인이나 기업의 태도가 아니라 무엇을 남겨야 하는지에 대한 합의의 부재다.

언론은 이 국면을 대체 서사로 소비했다. AI가 수학자를 밀어내는가, 수학이라는 직업은 끝났는가. 물리학자 알렉산더 위스너그로스가 자기 뉴스레터에 “수학은 끝났다”고 쓴 것도 그 프레임 안에서 널리 인용됐다. 그는 2025년 12월 31일자 회차에서 한 모델의 최상위 난도 수학 벤치마크 점수를 근거로 그렇게 적었다. 근거로 든 숫자는 FrontierMath 최상위 등급에서 받은 29.2%였고, 그는 2026년 1월 다보스 회차에서 같은 진단으로 돌아왔다. 벤치마크 점수 하나에서 한 분야의 종말을 읽어 내는 논법이다. 그런데 실제로 수학자들이 서로 다른 말을 한 지점은 거기가 아니었다.

가장 많이 인용된 전향은 토론토대 조교수 대니얼 리트의 내기 인정이다. 그는 2025년 3월 AI 연구자 타메이 베시로글루와 3대 1 배당으로 내기를 걸었다. 2030년까지 AI가 최상위 학술지 수준의 정수론 논문을 자율적으로 만들어 내겠느냐는 것이었다. 2026년 8월 그는 스스로 졌다고 선언했다. “엄밀히 말해 판정이 난 것은 아니지만, 그런 논문을 만드는 데 어떤 능력이 필요한지에 대해 내가 틀렸다는 것은 분명하다. 이제 시간문제일 뿐이다.” 계기는 야코비안 반례가 아니었다. 8월 초 Astra 발표였고, 본인은 그것조차 유일한 이유는 아니며 여러 모델을 직접 써 보면서 능력에 대한 감을 잡은 결과라고 밝혔다. 덧붙여 그는 자신이 “더 나은 대리지표를 골랐어야 했다”고 자평했다. 논문 한 편이라는 지표가 그가 진짜 궁금해하던 것을 재지 못했다는 뜻이다.

그는 서둘러 판정을 확정할 생각이 없다고 밝혔고, 지금 나온 결과들을 아직 진짜 정수론 논문으로 인정하지 않는다. 비슷한 수준의 논문이 두세 편은 더 나와야 완전한 예로 보겠다는 것이 그의 조건이다. 그러니까 이 전향은 “AI가 이미 해냈다”는 선언이 아니라 “내가 필요하다고 생각했던 능력의 목록이 틀렸다”는 인정에 가깝다.

그가 진짜 궁금해하던 것이 무엇인지는 다른 수학자들의 말과 겹쳐 놓으면 드러난다.

매튜의 문장과 유엔의 문장은 서로 다른 사건에 대한 반응인데, 요구하는 바가 같다. 결과가 맞다는 확인만으로는 부족하고, 그 결과가 어떤 길을 거쳐 나왔는지 이야기가 붙어야 한다는 것이다. 이 요구에는 낙관 쪽도 반대하지 않는다. 버자드가 기뻐한 것은 기계 검증이 하루 만에 끝났다는 사실이지, 과정을 몰라도 된다는 뜻이 아니다. 해리스의 비판도 결국 같은 자리를 가리킨다. 추론 과정을 부산물 취급하는 태도가 문제라는 것이다.

그러니까 수학계가 갈라진 축은 AI가 수학자를 대체하는가가 아니었다. 산출물에 과정이 붙어 있는가였다. 리트가 내기의 대리지표를 잘못 골랐다고 말한 것도 이 지점이다. 논문이 나오느냐 마느냐는 세기 쉬운 대신, 정작 그가 걱정하던 것을 재지 못한다. 그럴듯한데 검증되지 않은 결과가 분야를 뒤덮는 상황 말이다. 그리고 이 요구는 마음가짐으로 충족되지 않는다. 인프라가 있어야 한다.

공백을 지적하는 일은 쉽고, 이미 무엇이 지어지고 있는지 보는 일은 조금 더 품이 든다. 수학계는 지난 2년 사이 두 종류의 인프라를 동시에 세우고 있다. 하나는 결과가 참인지를 기계가 확인하게 만드는 형식검증이고, 다른 하나는 그 결과가 어떻게 나왔는지를 기록으로 남기는 관행이다. 둘은 자주 한 덩어리로 이야기되지만 하는 일이 다르다.

5.1형식검증이 닫는 것

형식화는 규모부터가 만만치 않다. 수학의 표준 형식화 라이브러리 Mathlib은 8년 동안 600명이 넘는 기여자가 매달려 쌓아 올린 100만 줄 단위의 코드다. 정리 하나를 기계가 읽는 언어로 옮기는 일은 그 위에 벽돌을 얹는 작업에 가깝고, 그래서 큰 정리 하나의 형식화가 몇 달에서 몇 년씩 걸려 왔다.

Lean 4로 대표되는 형식검증은 증명의 각 단계를 기계가 검사할 수 있는 언어로 옮긴다. 성과는 빠르게 쌓이고 있다. Harmonic의 Aristotle은 2025년 국제수학올림피아드 여섯 문제 중 다섯 문제를 사람 확인 없이 자동 형식검증으로 통과했다. 금메달 기준과 같은 성적이다. Math Inc.의 Gauss는 강한 소수정리의 형식화를 3주에 마쳤는데, 같은 프로젝트가 사람 손에서는 18개월 넘게 완결되지 못한 상태였다. Axiom Math는 자사 시스템이 만든 증명이 학술지 다섯 곳에 게재 수락됐다고 밝혔다. 다만 어느 학술지의 어떤 정리였는지, AI 사용 공시나 저자 표기를 요구받았는지 같은 구체적 조건은 공개되지 않았다.

5.2형식검증이 닫지 못하는 것

기계 검증에는 조용한 사각지대가 있다. 타입체커는 증명이 논리적으로 정합한지만 본다. 그 증명이 붙어 있는 명제가 원래 물으려던 수학을 제대로 담고 있는지는 보지 않는다. Lean Atlas 논문은 이 현상에 의미적 환각(semantic hallucination)이라는 이름을 붙였다. 형식화가 타입체커를 통과하고 증명까지 완성됐는데도 원래의 자연어 진술과 의미가 같지 않은 경우다. 논문은 다섯 가지 패턴을 정리한다. 정의가 어긋나는 경우, 가정이 빠지거나 더해진 경우, 목표 자체가 바뀐 경우, 한정사와 적용 범위가 틀어진 경우, 타입의 기본값 때문에 뜻이 달라지는 경우다. 실제로 에르되시 문제들을 Lean으로 옮기는 작업에서 잘못 형식화된 사례가 다수 발견된 바 있다.

5.3비교표에 새 열이 하나 생겼다

계보 쪽에서 벌어진 일은 훨씬 조용했지만 이 글이 보기에는 더 중요하다. 2026년 3월 한 수학자가 플라스마 물리의 평형 정리를 Lean으로 형식화한 논문을 냈다. 그는 자기 작업을 기존 형식화 프로젝트들과 비교하는 표를 실었는데, 그 표의 열 가운데 하나가 “로그를 공개했는가”였다. 프로버 종류, 팀 규모, AI가 맡은 역할과 나란히, 프롬프트와 커밋 기록의 공개 여부가 프로젝트를 비교하는 정식 항목으로 올라온 것이다.

아홉 개 항목 중 로그를 전면 공개한 것은 표를 만든 그 논문 자신 하나뿐이다. 사람이 직접 작성한 코드는 0줄, 인간이 넣은 프롬프트 229개와 git 커밋 213개가 저장소에 전부 아카이브돼 있고, 총비용 200달러에 10일이 걸렸으며 사람의 감독 시간은 약 50시간이었다. 이 정도면 다른 사람이 같은 작업을 처음부터 되짚어 볼 수 있다. 계보 원장이 실제로 어떤 모양인지에 대한 첫 번째 실물 견본이다.

비슷한 요구가 벤치마크 쪽에도 나타났다. 2026년 6월 진행된 First Proof는 연구 수준의 미해결 문제를 AI 시스템에 풀리고 수학자 약 서른 명이 이중맹검으로 심사하는 대회인데, 참가 조건에 출력과 로그와 코드 전부를 공개할 수 있어야 한다는 조항이 들어 있다. 시스템은 입력 토큰과 출력 토큰, 추론 토큰을 기록해야 한다. 결과는 열 문제 중 일곱 문제가 통과 등급을 받았고, 두 문제는 대폭 수정이 필요했으며, 한 문제는 완전히 실패했다. 네 개 시스템이 원샷 모드로 24시간 안에 답안을 제출했고, 그 답안을 판정하는 데는 6월 초 닷새가 걸렸다. 로그 공개를 규칙으로 못 박은 대회에서도 결과의 진위를 가리는 일은 여전히 수학자 서른 명의 시간으로 치러진다. IMProofBench는 데이터셋 자체는 오염을 막기 위해 비공개로 두면서도 모델과 API 설정, 평가 프롬프트는 공개한다.

수학계는 누가 시켜서가 아니라 자기 필요 때문에 계보 원장을 쓰기 시작했다. 비교표에 열이 생겼다는 사실 자체가 관행이 형성되는 중이라는 증거이고, 그 열의 아홉 칸 중 여덟 칸이 비어 있다는 사실이 지금의 수준이다. 학술지 정책도 아직 여기까지는 오지 않았다. 모델과 버전을 밝히고 검증 방법을 서술하라는 요구는 강화되는 추세지만, 2026년 중반 기준으로 프롬프트 로그의 전면 공개를 의무화한 주요 수학 학술지는 확인되지 않는다. 엘스비어는 도구와 모델의 기록을 보존하라고 요구하되 공개까지는 요구하지 않는다.

수학은 세상에서 검증 문화가 가장 엄격한 분야다. 결과가 참인지를 몇 세기에 걸쳐 확인하는 절차를 만들어 왔고, 발표된 증명이 나중에 무너지는 일을 부끄러워할 줄 아는 공동체다. 그런 곳에서도 산출 속도가 기록 인프라를 앞질렀다. 그렇다면 검증 문화가 그보다 훨씬 느슨한 곳에서는 이미 오래전에 같은 상태가 됐다고 봐야 한다.

학술 출판 전반의 숫자가 그 격차를 보여준다. 학술지 5,114곳과 논문 520만 편을 분석한 연구에 따르면, 학술지의 70%가 AI 사용에 관한 정책을 도입했고 대개 공시를 요구한다. 그런데 2023년 이후 논문 7만 5천 편 가운데 AI 사용을 명시적으로 공시한 것은 76편, 약 0.1%였다. 이 연구는 증명 생성이 아니라 AI 보조 집필을 다룬 것이므로 야코비안 사건과 같은 층위에 놓을 수는 없다. 그러나 규범이 선언되는 속도와 실제로 지켜지는 속도 사이의 간격을 재는 지표로는 충분하다. 정책을 두는 것과 기록이 남는 것 사이가 이만큼 벌어져 있다.

이 구조를 일반 데이터·AI 파이프라인의 언어로 옮기면 익숙한 문제가 된다. 모델이 만든 산출물을 제품이나 보고서에 올리는 조직은 곧 같은 질문을 받는다. 이거 어떻게 나온 겁니까. 그때 대답할 수 있으려면 산출물마다 최소한 다음 다섯 가지가 함께 남아 있어야 한다.

• • 입력 데이터의 출처 — 어떤 데이터가 들어갔고 그 데이터를 쓸 권리는 어디서 왔는가
• • 모델과 버전 — 어느 모델의 어느 시점 버전인가. 같은 이름의 모델도 몇 달 뒤엔 다른 물건이다
• • 생성 조건 — 프롬프트, 온도, 도구 접근 권한처럼 결과를 바꾸는 설정
• • 시도 이력 — 몇 번 만에 나왔고 버려진 시도는 무엇이었으며 사람이 어디서 개입했는가
• • 검증 경로 — 무엇으로 확인했고 그 확인이 무엇을 보장하지 않는가

이 목록이 추상적으로 들린다면 앞 장의 그 한 건을 다시 보면 된다. 프롬프트 229개, 커밋 213개, 비용 200달러, 기간 10일, 사람이 쓴 코드 0줄. 다섯 항목이 전부 채워진 형태가 실제로 이렇게 생겼다. 대단한 시스템이 필요한 것도 아니었다. 한 사람이 저장소 하나에 남긴 기록이다.

페블러스가 이 사건을 눈여겨보는 이유도 여기 있다. AI-Ready Data라는 말로 우리가 계속 이야기해 온 것은 깨끗한 데이터가 아니라 출처와 이력이 붙어 있는 데이터였다. 야코비안 사건은 그 주장을 산출물 쪽에서 되풀이한다. 결과가 맞아도 그 결과가 어떻게 나왔는지 재구성할 수 없으면 자산으로 쌓이지 않는다. 라이덴 선언이 요구한 것이 학습 단계의 동의와 귀속이었다면, 이번에 드러난 것은 추론 단계의 기록 공백이다. 입력의 계보와 산출의 계보가 함께 있어야 신뢰가 성립한다.

기록은 나중에 만들 수 없다. 감사나 분쟁이 시작된 다음에 소급해서 재구성하려면, 이미 사라진 프롬프트와 폐기된 중간 산출물과 기억나지 않는 개입 지점을 사람의 진술로 메워야 한다. 수학계가 하루 만에 반례를 믿을 수 있었던 것은 그 산출물이 운 좋게도 자기 검증을 품고 있었기 때문이다. 대부분의 결과는 그렇지 않다. 운이 나쁜 쪽이 기본값이라고 보고 설계하는 편이 낫다.

참고문헌

1차 자료·학술

• 1.Tao, T. (2026). A digestion of the Jacobian conjecture counterexample. terrytao.wordpress.com
• 2.Alpöge, L. (2026-07-19/20). 야코비안 추측 반례 게시물. X.
• 3.Litt, D. (2026-08). 내기 인정 게시물. X. x.com/littmath
• 4.Yanahama, K. & Sannai, A. (2026). Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization. arXiv:2604.16347. arxiv.org
• 5.Ilin, V. (2026). Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium. arXiv:2603.15929. arxiv.org
• 6.First Proof (2026). arXiv:2606.18119. arxiv.org
• 7.IMProofBench (2025/2026). arXiv:2509.26076. arxiv.org
• 8.Harmonic Team (2026). Aristotle / IMO 2025 형식검증. arXiv:2510.01346. arxiv.org
• 9.He, Z. & Bu, Y. (2025/2026). Academic journals’ AI policies fail to curb the surge in AI-assisted academic writing. arXiv:2512.06705. arxiv.org
• 10.Smale, S. (1998). Mathematical Problems for the Next Century (16번 문제).
• 11.Keller, O.-H. (1939). 야코비안 추측의 일반화된 진술. 원 문헌 미확인, 2차 출처 교차확인.

해설·언론

• 12.The Conversation (2026). ‘hello there the jacobian conjecture is false thanx’: why a tiny social media post has mathematicians rethinking AI. theconversation.com
• 13.Cook, J. D. (2026-07-21). Locally everywhere does not imply everywhere. johndcook.com
• 14.Fortune (2026-07-21). Mathematicians grapple with a ‘very rapid and very unsettling change’. fortune.com
• 15.Wissner-Gross, A. (2025-12-31, 2026-01-16). The Innermost Loop. theinnermostloop.substack.com
• 16.Mowshowitz, Z. (2026-08). OpenAI’s Unreleased Model Astra Solves Ten Major Open Mathematics Problems. thezvi.substack.com

페블러스 인접 글

• 17.페블러스 (2026-06-19). AI의 에르되시 추측 반증. blog.pebblous.ai · (2026-06-30) 라이덴 선언. blog.pebblous.ai · (2026-08-06) 추론은 하지만 발견은 못 한다. blog.pebblous.ai