인간 수학자, 반례 찾기에서 AI에 추월당하다

• ChatGPT와 Claude 계열 모델이 불과 몇 주 사이 Erdős의 단위 거리 추측, Grothendieck의 군 스킴 질문, Jacobian Conjecture에 반례를 만들었으며 일부는 Lean으로 검증됨
• OpenAI의 Sol은 Erdős 반례와 필요한 전역 유체론 결과를 3주 만에 120만 줄의 Lean 코드로 형식화했으며, 이는 9년간 작성된 mathlib 230만 줄의 절반이 넘는 규모임
• Grothendieck의 60년 된 질문에는 Sol이 12쪽짜리 반례를 찾고 Fable이 4시간 만에 1,076줄로 형식화해, 위수 4이지만 4에 의해 소멸하지 않는 군 스킴의 존재를 확인함
• 자동 형식화는 연구 속도도 크게 높여, Andrew Yang이 약 2주 동안 25만 줄의 Lean 코드를 작성하며 Fermat의 마지막 정리에 필요한 모듈러성 올림 정리 프로젝트를 사실상 완성함
• AI가 생성한 비형식적 수학을 그대로 신뢰할 수는 없지만, 추측을 정확한 Lean 명제로 만들면 증명과 반증을 기계적으로 검사할 수 있으며 인간은 반례에서 더 깊은 수학적 통찰을 끌어내야 함

---

Erdős 단위 거리 추측과 전역 유체론

• 2026년 5월 20일 ChatGPT가 이산기하학의 Erdős 단위 거리 추측을 반증함
  • 1960년대 Golod와 Shafarevich의 깊은 정수론 정리를 이용해 반례를 구성함
  • 여러 수학자가 논증을 사전에 검토해 타당하다고 판단했지만, 발표 당시 Lean 형식화는 없었음
• 5월 26일 필즈상 수상자이자 Logical Intelligence 최고과학책임자인 Mike Freedman이 자사 시스템으로 ChatGPT 논문 전체를 Lean에 자동 형식화했다고 알림
  • 형식화된 범위는 Golod–Shafarevich 정리가 Erdős 반례를 함의한다는 명제였음
  • 기반이 되는 정수론 정리 자체에는 100쪽 이상이 필요하며, 전역 유체론의 방대한 부분에 의존함
• 2025년 유체론 형식화 여름학교 이후 1년 동안 국소 사례는 거의 완성됐지만 전역 사례는 미해결 상태로 남아 있었음

Sol이 만든 120만 줄의 완전한 형식화

• 6월 26일 OpenAI의 Boris Alexeev가 새 모델 Sol을 유도해, 수학 공리 외에는 아무것도 가정하지 않는 Erdős 반례의 완전한 형식화를 만들었다고 Lean Zulip에 공개함
• Sol은 3주 동안 120만 줄의 Lean 코드를 생성함
  • 9년에 걸쳐 작성된 mathlib는 230만 줄임
  • 코드 품질은 고르지 않았지만, 전역 유체론의 어려운 결과와 수체의 코호몰로지에 관한 비자명한 정리를 실제로 증명함
• Lean은 임의 명령을 실행할 수 있는 프로그래밍 언어이므로, 악성 코드 가능성을 고려해 생성 코드를 샌드박스에서 실행함
• 이 규모와 속도는 대규모 AI 생성 수학 개발이 불가피하다는 판단으로 이어짐

Formalizing Fermat 워크숍과 도구 접근성

• 7월 6~10일 열린 Formalizing Fermat 워크숍에는 25명이 참석했지만, 후원사 Logos Research의 자동 형식화 시스템은 동시에 5명만 사용할 수 있었음
• 모든 참석자에게 한 달짜리 Claude Max 구독을 제공해 Claude Fable을 쓸 수 있게 했고, OpenAI도 한 달짜리 ChatGPT Pro 접근권을 무료로 제공함
  • Sol은 7월 9일 출시 예정이었음
  • Fable은 7월 7일 종료될 예정이었지만 실제 접근은 유지됨
  • 참석자들은 워크숍 5일 중 4일 동안 Sol과 Fable을, 전체 기간에는 Logos 도구를 이용할 수 있었음
• Fermat의 마지막 정리 형식화에 필요한 유한 평탄 군 스킴 이론을 개발하기 위해 고전 논문들을 Fable과 ChatGPT에 입력하고 자연어 해설을 작성하게 함
  • Logos는 해설에 포함된 한 명제가 거짓임을 찾아 명시적인 반례를 내놓음
  • 확인 결과 표준 구성을 기술한 LLM 생성 문서가 잘못돼 있었으며, 사람은 읽는 과정에서 오류를 놓쳤음
  • 단순히 논증을 이해하지 못한다고 답하는 대신 논증이 틀렸다는 증명을 제공했다는 점에서 차이가 있었음

Grothendieck의 군 스킴 질문

• UChicago 교수 Akhil Mathew는 모든 위수 (n)의 유한 자유 군 스킴이 (n)에 의해 소멸하는지를 묻는 Grothendieck의 오래된 질문을 AI에 제안함
  • Deligne은 가환인 경우를 증명함
  • Grothendieck은 밑공간이 reduced인 경우를 증명함
  • Rene Schoof가 더 많은 사례를 다뤘고, Emiliano Torti도 전년도 논문에서 더 일반적인 경우를 증명함
• 워크숍 다음 날인 7월 11일 Sol이 반례를 찾아 12쪽짜리 PDF를 생성함
  • 비형식적 결과 대신 전체 Lean 형식화를 요청하자 Fable이 4시간 만에 1,076줄로 자동 형식화함
• Lean 파일에 파일 삭제 같은 명령 없이 정리만 담겼는지 먼저 검사한 뒤 노트북에서 컴파일함
  • 명제에 mathlib의 개념만 사용됐는지 확인함
  • 명제가 실제로 반례의 존재를 나타내는지 점검함
  • 증명이 정상적으로 컴파일되는지 검사함
  • 전체 검증에는 5분이 채 걸리지 않았음
• 검증 결과 위수 4이지만 4에 의해 소멸하지 않는 군 스킴이 존재함
• Akhil Mathew는 이 반례를 mathlib PR로 제출함
• Erdős 반례는 약 100만 줄인 반면 Grothendieck 반례는 약 1,000줄로 훨씬 단순했지만, 60년 된 대수기하학 질문을 기계가 해결한 사례가 됨

전문가 반응과 모듈러성 올림 정리

• 7월 14일 Imperial College의 한 교수는 Grothendieck 반례가 쉽게 발견됐다는 사실이 인간이 해당 문제를 충분히 오래 생각하지 않았음을 보여줄 뿐이라고 평가함
• 박사과정 학생 Andrew Yang은 Fermat의 마지막 정리에 중요한 모듈러성 올림 정리를 Lean으로 형식화하면서 Sol과 Fable을 사용함
  • 약 2주 동안 25만 줄의 Lean 코드를 작성함
  • 이를 통해 프로젝트를 사실상 완성함
• Imperial의 다른 교수는 대학원생들이 Sol과 Fable에 월 200달러를 지불하는 것을 이해하기 어렵다고 봤지만, 이 성과를 확인한 뒤에는 오히려 도구에 월 200달러를 쓰지 않는 박사과정생이 비합리적이라고 판단함
• Harvard는 이미 모든 박사과정생, 박사후연구원, 교수에게 Fable 무료 접근권을 제공하고 있었음

Jacobian Conjecture 반례

• Akhil Mathew와 Levent Alpöge는 대수기하학에서 추가 반례를 찾는 방안을 논의했고, Fable이 약 100년 동안 열려 있던 유명 문제인 Jacobian Conjecture의 반례를 찾음
• Levent Alpöge는 2026년 월드컵 결승전 도중 해결된 것으로 보이는 결과를 X에 공개함
• Akhil Mathew가 새 mathlib PR을 제안했을 때는 Paul Lezeau가 이미 반례를 수동으로 형식화해 DeepMind의 Formal Conjectures 저장소에 PR을 제출한 뒤였음
• mathlib에는 수학 추측의 대규모 목록이 없지만, Formal Conjectures 저장소는 이를 보유함
• 사람이 추측의 뜻을 충실히 담은 Lean 명제에 합의하면, AI가 생성한 코드가 그 추측을 증명하거나 반증하는지 확인하는 작업은 간단해짐

형식 검증 이후 인간에게 남은 과제

• Jacobian Conjecture에서는 인간이 해당 반례에서 정확히 무슨 일이 일어나는지 이해하는 작업이 다음 단계임
• Grothendieck 반례 역시 임의의 환 표현과 계산을 나열하는 수준을 넘어 더 깊이 이해하려는 작업이 진행 중임
• 반례의 가치는 문제를 형식적으로 끝내는 데 그치지 않으며, 인간이 수학을 더 잘 이해할 수 있도록 통찰을 추출하는 과정에서 완성됨

[GN⁺]

Lobste.rs 의견들

• 정말 놀라운 결과임. 작년 다변수 미적분학 교수가 보너스 문제로 농담처럼 냈을 만큼 유명하고 접근하기 쉬운 추측임
  대수기하학에 익숙하다면 사후적으로 반례를 구성하는 꽤 자연스러운 경로가 보이며, LLM도 이런 직관을 제시할 수 있어 난데없이 나온 반례는 아님. 또한 돌이켜 보면 추측이 거짓임을 암시하는 단서도 있었고, 이전부터 변형된 추측에 대해 인간이 만든 반례가 존재했음
  이번 반례는 세 변수 함수 C^3 → C^3이며 2차원 추측은 여전히 미해결임. 2차원 반례가 존재한다면 이번 것과 달리 상당히 복잡해야 한다는 결과도 있음
  그렇더라도 수학자들이 오랫동안 연구해 온 유명한 추측이라는 점에서 대단한 성과임. 단위 거리 추측과 달리 참인지에 대한 전문가 견해도 갈렸으므로, 그동안 아무도 반례를 찾지 않았던 것도 아님. 무차별 대입으로 발견할 수 있는 결과가 아니며 모델이 반례를 맹목적으로 열거한 것은 분명히 아님

• LLM 주도 프로그램 탐색이 나아갈 길처럼 느껴짐. 단일 커널을 형식화하는 작업도 엄청났지만, 이제 모듈의 형식적 정확성 속성을 명시하고 증명된 구현을 도출하는 꿈에 훨씬 가까워진 듯함
  어떤 정리를 선택해 형식화할지, 구현을 실용적으로 이끌 방법을 정하는 데는 여전히 인간의 창의성이 많이 필요하며 그 가능성이 매우 흥미로움

• 야코비안 추측은 수학의 미해결 문제 상위 100개에 충분히 들지만, GPT의 단위 거리 추측은 아마 상위 1,000개 정도일 것임. 20세기 말 힐베르트 문제의 후계자로 여러 목록이 제안됐고, Millennium Prize Problems가 가장 널리 인정받았지만 Smale의 문제도 그에 가까웠으며 야코비안 추측이 여기에 포함됨
  다만 2차원 문제가 여전히 열려 있으므로 AI가 힐베르트 문제의 20세기판인 Smale의 문제 하나를 풀었다고 표현하면 곤란함. 푸앵카레 추측도 5차원 이상은 1961년, 4차원은 1982년에 증명됐지만 핵심인 3차원은 2003년에야 해결됐음
  많은 수학자가 야코비안 추측이 3차원 이상에서는 거짓이라고 봤으며, 이는 사후 합리화가 아님. 비전문 분야 수학자의 관점을 보여주는 Peter Woit의 2004년 글도 “야코비안 추측은 대수기하학에서 가장 유명한 미해결 문제 중 하나이며, Carolyn Dean이 복소 변수 두 개의 다항식에 대해 증명한 듯함. 변수가 더 많으면 참이 아니라고 믿는 사람도 많다”고 적었음

• 수학자는 아니지만 취약점 탐색과 반례 탐색에는 겹치는 부분이 있을 듯함. 둘 다 복잡한 시스템이 잘못 동작하게 만드는 방법을 찾는 과정임

  • 맞는 직관임. SMT 솔버로 형식 검증을 할 때 검사할 코드 주변에 사전 조건과 사후 조건을 입력하며, 이를 호어 삼중항(Hoare triple)이라고 함. SMT 솔버가 조건을 만족하지 않는 입력을 찾으면 문자 그대로 반례라고 부름
    형식 검증 회사에서 일할 때도 탐색 결과를 버그나 취약점보다 반례라고 불렀음. 결과는 명세에 따라 달라지므로 이 표현이 더 정확함. 언어나 컴파일러의 정확성 문제라도 실제 버그인지 의도된 기능인지는 명세 없이는 판단하기 어려움
  • 대부분의 테스트가 경험적 검사인 이유도 같음. 경험적 연구처럼 명제를 증명하려는 게 아니라 반례를 찾는 과정임

• 악성 Lean 코드가 임의 명령을 실행할 수 있다면, 과거로 돌아가 Lean이 임의 명령을 실행하지 못하도록 다시 만들고 싶음. 정리 증명 언어가 셸 스크립트를 실행해야 하는 타당한 용도에는 상위 집합이나 추가 권한을 제공하고, 그 언어는 Bloated라고 부르면 됨

  • Lean에는 모나드가 있고 본질적으로 순수 함수형이어야 할 듯함. 따라서 주 정리의 타입이 Lean의 IO에 해당하지 않는지 확인하고 unsafePerformIO에 해당하는 기능의 사용 여부를 검사하면 될 것 같음. 다만 다른 수상한 탈출구가 있는지는 모르겠음
  • Rust의 unsafe 같은 구조를 도입하고, 위험한 구문을 허용하려면 --unsafe-allow-unsafe 같은 추가 인자를 요구하면 좋을 듯함. 많은 도메인 특화 언어(DSL)도 이런 식으로 언어를 분리하면 이점을 얻을 수 있음

[GN⁺]

Hacker News 의견들

• 대학원 시절 지도교수의 연구 수업에서 열린 문제에 직접 기여할 기회가 있었음. 어느 금요일 교수는 참이길 바라는 매끄럽고 아름다운 추측을 제시했지만, 기묘한 예외를 좋아하고 증명 도구도 부족했던 나는 반례를 찾는 데 집중해 한 시간 만에 발견함
  교수는 주말 내내 증명에 실패했는데, 서로 다른 도구·기대·동기를 지닌 사람이 같은 문제를 보면 전혀 다른 방향에서 기여할 수 있음을 보여준 일임. 위대한 지도교수에 비할 수는 없었지만, 그때만큼은 다른 방향을 볼 이유가 있었고 그것이 내 유일한 수학 연구 기여인 작은 반례로 이어짐

  • 기계가 반례를 잘 찾는 이유도 여기에 있을 듯함. 추측에 대한 미적 집착도 없고 추한 결과를 내놓는 데 부끄러움도 없음
  • 수학자로서 내 체감은 반대임. 증명은 아는 증명을 조금 변형하면 되지만, 반례를 만들려면 대상의 구조를 깊이 이해해야 해서 내 능력을 넘어설 때가 많음
    다만 이는 내가 이해하기 어려운 추상적 대상을 주로 다루기 때문일 수 있고, 수나 다항식에서는 반대일 가능성이 큼
  • 학생에게 아직 풀지 못한 문제를 공개하고 참여를 권하는 교수·연구자·교사는 더 높이 평가받아야 함. 대학 첫 공학 수업에서 강사가 1학년들에게 “우리가 아직 풀지 못한 문제들이니 아이디어가 생기면 알려 달라”고 했을 때 어느 때보다 환영받고 공동체에 포함된 느낌이었고, 자칫 따분할 수 있는 학업 초반에 큰 영감을 줬음
  • 《How to Solve It》에도 거의 같은 이야기가 있음
  • 더 극단적이면서 반대 방향인 Zeeman의 일화가 있음. 그는 5차원 공간에서 매듭지어진 구를 찾으려고 수년을 보냈다가 불가능하다는 사실을 깨닫고 몇 시간 만에 증명함
    https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

• 쌍둥이 소수 추측으로 유명한 Yitang Zhang은 Purdue에서 Tzuong-Tsieng Moh의 지도를 받으며 야코비안 추측을 7년간 연구함. 학위논문의 핵심 단계가 Moh의 잘못된 따름정리에 의존한 것으로 드러났고, Moh는 추천서 작성을 거부했으며 Zhang은 교육·연구직을 구하지 못해 수년간 Subway에서 일하게 됨
  1986년 연구를 시작할 때 ChatGPT가 있었다면 어땠을지 궁금함. 지금은 감동적인 성공담이 됐지만, “庾信平生最萧瑟，暮年诗赋动江关”이라는 시구처럼 복잡한 감정을 불러일으킴

  • 수학 박사학위 발표 중 심사 교수가 증명의 결함을 발견한 적이 있음. 학생이 이해한 뒤 “이제 어떻게 하죠?”라고 묻자 심사 교수는 그저 어깨를 으쓱했음
  • 훗날 쌍둥이 소수 추측에서 성공했으니 감동적이라고 할 수는 있겠지만, 학계의 이런 이야기에 지쳤음. 정치와 평판 관리가 지나치게 많고 Zhang은 그런 고통을 겪지 말았어야 함
    수학 쪽으로 연구를 넓히며 문헌 속 명제 중 상당수가 거짓이고 응용 문헌에까지 광범위하게 전파됐다는 데 놀랐음. 문제를 알려도 Zhang의 일화처럼 방어와 부정으로 대응하는 경우가 많음. LLM은 증명에 유용하지만 크게 틀리기도 하며, 다른 직관으로 탐색 방향을 제안하는 또 한 사람과 비슷해서 1986년에도 결과는 같았을 듯함
  • ChatGPT가 옮긴 시의 뜻은 “Yu Xin의 삶은 철저히 쓸쓸했으나, 노년의 시와 부가 강호를 뒤흔들었다” 정도임

• 수학에서 반례는 정의를 다듬고 증명을 날카롭게 만드는 데 매우 중요함. Imre Lakatos의 1976년 저서 《Proofs and Refutations》를 추천하며, 위상수학·확률론·해석학 등에는 반례만 다루는 책도 상당히 많음
  https://en.wikipedia.org/wiki/Proofs_and_Refutations
  https://www.amazon.com/s?k=counterexamples

• 반례를 찾으면 거짓인 명제를 증명하느라 시간을 낭비하지 않고 다른 문제로 넘어갈 수 있으므로, 적어도 수학에서는 인류의 시간을 더 생산적으로 쓰게 해줌

  • 반례에 의한 반증은 효과적이지만 궁극적으로는 만족스럽지 못함. 답은 주지만 수학이 왜 그렇게 작동하는지 이해하게 하거나 새로운 질문으로 이끌지는 못함
    무엇이 우아하고 통찰력 있는 증명인지 인간이 판단하는 동안에는 인간 수학자의 일이 남아 있을 것임
  • 반례는 정리의 명제를 다듬는 데도 유용함. 이론 컴퓨터과학 연구에서는 참이길 바라는 정리를 증명하다 반례를 찾고, 명제를 수정한 뒤 계속하는 과정이 흔함
    컴퓨터과학의 많은 정리가 귀납적·공귀납적 정의를 다룬다는 점도 도움이 됨
  • 특히 반례가 형식 검증됐다면 수년간의 추측성 노력을 거의 즉시 확정적 답으로 바꿔줌
  • 하지만 전체적으로 시간이 더 생산적으로 쓰였다고 단정할 수는 없음. 명제를 증명하든 반증하든, 최종적으로 참이든 거짓이든 그 과정에서 새로운 통찰이 생길 수 있음

• 수학판 《John Henry의 발라드》도 AI가 쓰게 될 듯함. 기계조차 능가하지 못하는 “THE BOOK에 실릴 법한” 증명을 내놓을 마지막 인간 챔피언이 누가 될지 궁금함
  https://en.wikipedia.org/wiki/John_Henry_(folklore)
  https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

  • 이는 축구 팬처럼 수학을 경쟁으로 보는 건강하지 못한 관점임. 수학에서 가장 가치 있는 것은 아름다운 증명만이 아니라 유용한 정의이며, 좋은 정의와 그로부터 좋은 추측을 만드는 일은 LLM이 아직 정복하려 하지 않은 영역임
  • 아직 그렇게 극적이지는 않지만 곧 그 단계에 이를 가능성은 있음. AI 능력이 점근적으로 발전할지 가속할지 구조적으로 예측할 근거가 없고, 어떤 문제가 새 방법에 풀릴지도 양쪽 가능성이 모두 열려 있음
    AI 능력의 내부와 성장 곡선을 이해하지 못하며, 의도적으로 성능을 낮춰 보이는지조차 정확히 알 수 없음. 측정에 저항하는 창발 현상일 수도, 몇 년 뒤 시계처럼 예측 가능해질 수도 있음. 아는 사람은 없고, 있다면 말하지 않으며 목소리 큰 사람들도 아는 게 없음

• 대학원생의 의미 있는 성과를 크게 앞당긴다면 학생당 연 $2,400을 투자하지 않을 이유가 없음. 전체 비용에서 보면 푼돈에 가까움

  • 일부 대학원생은 자신을 “의미 있는 결과를 생산하는 기계”가 아니라 윤리적 존재로 봄. 유용한 LLM도 도용된 학습 데이터와 막대한 환경 영향 때문에 정당화하기 어렵다는 점을 모두 알고 있음
  • EPSRC 박사과정의 생활비 장학금은 약 £20,000이므로 연간 비용의 약 10%에 해당함. 학생 개인에게는 큰 부담임

• 대학 시절 LLM이 만든 Lean 형식화가 있었다면 좋았을 것임. 강의 슬라이드의 수학에는 오류가 많았고, 일부 교수는 “증명은 슬라이드에 있다”며 해명 요구를 거절하면서도 오류를 인정하는 데 인색했음
  Lean 증명 자체는 이해에 적합하지 않은 경우가 많지만, 이를 바탕으로 사람이 이해하기 쉬운 논증을 생성할 수 있기를 바람

  • 첫 주장에는 동의하기 어려움. 학습 곡선은 가파르지만 잘 작성된 Lean·Agda·Rocq 형식화는 증명을 이해하는 데 탁월함. 좋은 형식화는 개요와 핵심 논증을 구조적으로 보여주고, 종이 증명과 달리 원하는 깊이까지 모든 단계의 세부 사항을 확인하게 해줌
    Martín Escardó의 TypeTopology Agda 저장소가 좋은 예임. 반면 현재 LLM이 생성한 형식화는 매우 난잡할 수 있어 참을 인증하고 흥미로운 논증을 담더라도 수학적 이해를 높이는 형태로 다듬는 데 상당한 작업이 필요함. 대화형 Agda 튜토리얼은 lets-play-agda.quasicoherent.io에 있음
  • 형식화는 논쟁을 끝내고 의심을 완전히 제거하는 Leibniz식 접근에도 쓸 수 있음

• 수학자에게 반례는 물리과학의 예상 밖 결과처럼 당장은 성가셔도 모델의 부정확성을 드러내 엄청나게 중요할 수 있는 것인지, 아니면 프로그래밍의 버그 보고처럼 사소하고 귀찮은 세부 사항인지 궁금함

  • 반례는 조건의 역할을 명확히 해줌. 증명의 각 조건을 위반했을 때 무엇이 실패하는지 보여주는 가장 단순하고 기억하기 쉬운 반례가 있으면 매우 유용함
    수학자들은 머릿속에 반례 동물원을 가지고 다니는 경향이 있음. 정리를 복원할 때도 날카롭고 기억에 남는 반례를 떠올리며 그것들을 배제하도록 정의역과 조건을 좁힐 수 있음
  • 《Counterexamples in Topology》와 《Counterexamples in Analysis》처럼 반례를 통해 분야의 미묘한 차이를 가르치는 교육서가 있음. 의도된 정상적 대상만 배우는 것보다 병리적·퇴화한 예시에서 세부 사항을 익히기 쉬워 인기가 많음

• 이 수학의 상당 부분은 이해하기 어렵지만 대체로 정리 증명을 다루는 듯함. AI 수학이 계속 가속하면 장차 공학이나 생의학에 응용될 새로운 수학까지 발견할지, 인류의 거대한 돌파구 직전인지, 아니면 이미 알려진 것을 증명하는 데 그칠지 궁금함

  • 가능성은 있음. 압축 센싱은 생의학에 응용되는 새로운 수학의 예로 볼 수 있고, MRI 촬영 시간을 크게 줄여 환자 경험을 개선하고 더 많은 환자가 검사를 받게 할 수 있음
    https://en.wikipedia.org/wiki/Compressed_sensing
  • 공학과 생의학에는 적용되더라도 아마 장기적인 일이겠지만, 새로운 수학적 방법의 발전은 기초물리학 연구에 더 일찍 중요해질 수 있음. 우주 모형의 표현이나 검증을 가능하게 한 수학 도구가 등장하면서 모형이 크게 개선된 적이 종종 있음
  • 가능하더라도 아주 오래 걸릴 것임. 대부분의 응용 분야에서는 수백 년 전 수학조차 이제야 제대로 활용하기 시작한 수준임

• 언젠가 수학자들이 검토해야 할 증명에 파묻혀 과신한 거짓 명제가 수학계에 들어올 수 있음. 미래 수학자는 AI를 쓰는 소프트웨어 엔지니어처럼 AI 생성 증명 수천 줄을 검사하며 미묘한 오류를 찾게 될지도 모름

  • 그 시점은 이미 오래전에 왔음. 오늘날 문헌은 방대하고 잘못된 증명으로 가득하며, 출판된 결과 중에도 수는 알 수 없지만 확실히 0은 아닌 만큼 거짓 결과가 섞여 있음