테렌스 타오가 보는 증명 검사기와 AI 수학 코파일럿

 (scientificamerican.com)
1P by GN⁺ | ★ favorite | 댓글 1개
  • 수학 증명이 더 엄격하게 형식화되면서, Lean 같은 도구가 사람의 증명을 검증하고 대규모 협업의 신뢰 기반을 바꾸고 있음
  • mathlib 같은 표준 라이브러리가 쌓이자 학부 수준 정리부터 새로운 분야까지 형식화하는 진입 장벽이 낮아지는 중임
  • PFR 추측 형식화에서는 20명 넘는 참여자가 작은 증명 단계를 나눠 맡았고, 테렌스 타오는 줄 단위 검토보다 전체 방향 관리에 집중함
  • AI는 당장 수학을 “해결”하기보다 증명 코파일럿으로 형식화·검증·반복 작업을 돕는 역할에 가까움
  • 수학 연구는 사람의 방향 설정, 세부 형식화, AI 훈련, AI 증명의 해석처럼 더 명시적이고 분업화된 작업으로 바뀔 수 있음

형식화가 바꾸는 수학 협업

  • 전통적인 수학 연구는 소수 협업에 가까웠고, 타오는 보통 5명 정도가 협업 규모의 상한에 가깝다고 봄
  • 자동 증명 검사기(proof checker)가 있으면 서로 모르는 수백 명과도 협업할 수 있음
    • 기여자는 코드를 올리고, Lean compiler가 검증함
    • 신뢰를 개인적 관계에만 의존하지 않고, 형식 검증 결과로 확인할 수 있음
  • Polynomial Freiman-Ruzsa(PFR) 추측의 최근 결과를 형식화할 때는 20명 이상이 참여함
    • 증명을 많은 작은 단계로 나눔
    • 각 참여자가 한 단계의 증명을 맡음
    • 타오는 모든 기여를 줄마다 확인하기보다 전체 진행 방향을 관리함

모든 수학자가 프로그래머일 필요는 없음

  • 형식화 프로젝트에서는 역할 분담이 가능함
    • 어떤 사람은 수학적 방향에 집중함
    • 어떤 사람은 작은 수학 조각을 형식 증명으로 바꾸는 일을 전문적으로 맡음
  • Peter Scholze처럼 컴퓨터에 익숙하지 않은 수학자도 Lean 프로젝트에 참여할 수 있음
  • 큰 수학 과제를 작은 조각으로 나누면 전체 이론을 모두 이해하지 않아도 특정 하위 작업에 기여할 수 있음

Lean, mathlib, 검색이 만든 실용성

  • 형식 수학이 실용화된 큰 이유 중 하나는 표준 수학 라이브러리의 발전임
  • Lean에는 mathlib라는 대규모 프로젝트가 있음
    • 미적분, 위상수학 같은 학부 수학의 기본 정리가 하나씩 라이브러리에 들어감
    • 목표는 라이브러리를 대학원 수준까지 끌어올리는 것임
    • 그렇게 되면 새로운 수학 분야를 형식화하기 쉬워짐
  • 증명을 만들려면 이미 참으로 확인된 정리를 찾아야 하므로, 더 똑똑한 검색 엔진도 중요해짐
  • PFR 프로젝트 전체를 형식화한 뒤 검증 컴파일에는 약 30분밖에 걸리지 않음
    • 병목은 컴퓨팅 파워보다 사용성, 사용자 친화성, 사람들의 도구 적응에 있음
  • Lean은 현재 가장 활발한 커뮤니티를 가진 형식 언어로 평가됨
    • 단독 저자 프로젝트에는 다른 언어가 더 나을 수 있음
    • Lean은 배우기 쉽고, 라이브러리와 커뮤니티가 좋음
    • 나중에 다른 대안으로 대체될 수 있지만 현재는 지배적인 형식 언어임

아직 높은 형식화 비용

  • 타오는 어떤 프로젝트를 형식화할 수는 있지만, 현재는 자신의 시간을 한 달 써야 할 수 있다고 봄
  • 모든 결과를 일상적으로 형식화할 단계는 아직 아님
    • Lean을 배우는 데 도움이 되는 경우
    • 결과의 정확성에 대한 관심이 큰 경우
    • 형식화가 실제 가치를 주는 프로젝트를 골라야 함
  • 기술이 나아지면 형식화 비용은 줄어들 수 있음
    • 지금은 기존 방식보다 10배 오래 걸릴 수 있음
    • 앞으로는 2배 정도, 나아가 1배 미만까지 줄어들 가능성이 있음

AI는 수학자의 코파일럿이 될 수 있음

  • 타오는 미래에 수학자가 증명을 직접 타이핑하기보다 GPT 같은 시스템에 설명하고, AI가 진행 중에 Lean 형식화를 시도하는 방식을 상상함
    • 검증이 통과되면 LaTeX 논문과 Lean 증명을 함께 제공할 수 있음
    • 사용자가 원하면 저널 제출까지 돕는 조수가 될 수 있음
  • 현재 가장 빠른 형식화 경로는 여전히 사람이 먼저 증명의 아이디어와 초안을 만드는 것임
  • 장기적으로는 사람이 전체 증명을 모르는 상태에서 작은 조각들을 형식화하고, AI와 사람이 함께 연결해 큰 정리를 증명하는 프로젝트도 가능할 수 있음
    • 타오는 이런 방식이 가능해지려면 여러 해가 걸린다고 봄
    • 현재 기술은 아직 부족하고, 형식화도 여전히 고통스러운 작업임

“수학이 해결된다”는 전망과의 거리

  • Tony Wu와 Christian Szegedy는 2~3년 안에 기계가 인간보다 증명을 더 잘 찾는다는 의미에서 수학이 “해결”될 것이라고 말한 바 있음
  • 타오는 3년 안에 AI가 수학자에게 유용해지고 뚜렷한 진전이 있을 수는 있지만, 수학이 해결된다고 보지는 않음
  • AI는 증명 중 한 단계가 참인 것 같지만 사람이 바로 보지 못할 때 도움을 요청하는 코파일럿이 될 수 있음
  • AI가 현재 인간이 하는 수준의 수학을 수행하더라도, 인간 수학자는 더 높은 수준의 수학으로 이동할 수 있음
  • AI를 통해 한 번에 수백 개나 수천 개의 정리를 증명하는 방식도 가능해질 수 있음
    • 인간 수학자는 AI가 무엇을 할지 지휘하는 역할을 맡음
    • 타오는 이런 변화의 시간표를 2~3년으로 보는 전망은 다소 공격적이라고 봄

증명 이해와 AI 생성 증명

  • 수학 증명은 단순히 참을 확인하는 절차가 아니라, 왜 참인지 이해하는 과정이기도 함
  • 가까운 미래에는 AI가 지루하고 사소한 일을 먼저 자동화하고, 인간이 여전히 방향을 잡을 가능성이 큼
  • AI가 이해하기 어렵고 보기 흉한 증명을 내놓으면, 사람은 그 증명을 다시 분석할 수 있음
    • 예를 들어 10개의 가정으로 결론을 얻는 증명에서 가정 하나를 빼도 성립하는지 확인할 수 있음
  • AI 생성 증명에서 통찰을 추출하는 새로운 유형의 수학자가 생길 수 있음
    • 초기 AI 증명에는 통찰이 없어 보일 수 있음
    • 사람들은 그 증명을 더 이해 가능하게 만들고 구조를 찾아낼 수 있음

풀리지 않은 문제와 AI의 한계

  • 미해결 추측을 증명하려면 먼저 더 작은 조각으로 나누는 일이 필요함
  • 문제를 더 쉬운 문제로 바꾸는 것보다 더 어려운 문제로 바꾸는 일이 훨씬 쉬움
  • 타오는 AI가 이 분해 작업에서 인간보다 낫다는 능력을 아직 보이지 못했다고 봄
  • AI가 여러 분야 사이의 연결 가능성을 제안하는 용도는 흥미로움
    • 현재 성공률은 낮음
    • 10개 제안 중 1개만 흥미롭고 9개는 쓸모없을 수 있음
    • 타오는 미래에는 이 부분이 바뀔 수 있다고 봄

수학 지식의 데이터 문제

  • 수학 AI 훈련의 문제 중 하나는 충분한 데이터가 없다는 점임
  • 온라인 논문은 훈련에 사용할 수 있지만, 많은 수학적 직관은 논문에 담기지 않음
    • 수학자 사이의 대화
    • 강의
    • 학생을 지도하는 방식
    • 실패한 시도와 수정 과정
  • 출판된 증명은 압축된 결과물이며, 사람들은 성공 사례만 출판하는 경향이 있음
  • 정말 귀한 데이터는 무언가를 시도했지만 잘 되지 않았고, 어떻게 고쳤는지를 담은 과정임
  • 미래에는 연구 시도와 실패 과정이 기록되어 AI 훈련이나 다른 연구자의 중복 실패 방지에 쓰일 수 있음
    • 타오는 2040년의 고급 AI Lean 같은 시스템을 쓰기 위해 연구 과정 기록에 동의하는 상황을 예로 듦

더 명시적인 수학으로 가는 변화

  • 많은 수학 지식은 개별 수학자의 머릿속에 갇혀 있고, 아주 작은 일부만 명시적으로 남음
  • 형식화가 늘수록 암묵적 지식이 더 많이 명시적 지식으로 바뀜
  • 형식화된 교과서는 대화형 교과서로 이어질 수 있음
    • 높은 수준의 증명 설명에서 시작함
    • 이해되지 않는 단계는 더 자세히 펼쳐볼 수 있음
    • 원하면 공리 수준까지 내려갈 수 있음
  • 이런 방식은 한 분야의 수학자가 다른 분야에 기여하기 쉽게 만들 수 있음
    • 큰 과제의 하위 작업을 정확히 지정할 수 있음
    • 전체를 이해하지 않아도 필요한 조각에 참여할 수 있음

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • https://archive.is/Idouw

  • project manager mathematicians라는 표현이 Edsger Dijkstra가 1975년에 쓴 풍자문 “A letter to my old friend Jonathan” [1]과 후속 글 [2]을 떠올리게 함
    소프트웨어를 만드는 방식이 수학에 적용되면 얼마나 우스꽝스러울지를 보여주며 비판한 글이었지만, 어떤 면에서는 선견지명이 있었음
    핵심은 지식재산권, 특히 수학적 진리에 지식재산권을 적용하는 부조리를 비판하는 것이었고, 다행히 지금의 기계화 흐름에서는 그 부분이 큰 걱정은 아닌 듯함
    [1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
    [2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...

    • LLM도 수학을 할 수 있음. 형식화하지 않는다면 이 논문이 현재 최고 수준에 가까운 듯함: https://arxiv.org/abs/2301.13867
    • 그 비교는 말이 안 되는 듯함. 소프트웨어의 99.999% 는 최첨단이 아니라 관리 가능한 공학적 구현임

  • 통찰력 있는 글이지만, 빠진 부분은 LLM이 점점 초인간적인 방식으로 추상화한다는 점이라고 봄
    Tao는 “문제를 더 어렵게 바꾸기는 쉽지만 더 단순하게 바꾸기는 어렵고, AI가 인간보다 이 점에서 낫다는 걸 보여준 적은 없다”고 했지만, LLM의 작동 방식상 훨씬 높은 수준의 통찰이 가능해질 수 있음
    지금은 도우미, 사실 확인자, 지루한 일 처리자에 가깝지만 곧 통찰을 제안하는 존재가 될 것임. 이미 LLM은 임베딩과 지식을 압축하며 우리가 보지 못하는 통찰을 갖고 있음
    Hinton이 핵폭탄과 퇴비 더미의 관련성을 예로 드는 장면: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s

    • LLM의 가장 큰 문제는 인터넷에 있는 수많은 인간 글의 회귀 모델에 불과하다는 점임
      인간이 글 쓰는 방식을 흉내 내도록 학습된 기계일 뿐이고, 인간보다 똑똑한 무언가를 흉내 내는 데 필요한 학습 데이터가 없음
      기계학습이 인간 지능을 넘을 거라는 데는 의심이 없지만, 병목은 전 세계 글 전체에 회귀하는 대신 인간 개입 없이 자기 출력으로 스스로 학습하게 만드는 방법을 찾는 것임
      Ramanujan은 정규 교육도 없고 수학책 몇 권만 접하고도 빛나는 수학적 발견을 했는데, 기계학습 모델의 학습 데이터 관점에서는 거의 아무것도 아닌 양임
    • Hinton의 예시는 와닿지 않음. 취미로 정원을 가꾸기 때문에 “핵무기와 퇴비 더미의 공통점은?”이라는 질문에 바로 임계질량을 떠올렸음
      단어로 정리하는 데 10초쯤 걸렸지만, 필요한 정보를 알고 있으면 답은 명백했음
      Hinton은 이것이 유추적 사고를 보여준다고 하지만, 정원 관련 글과 퇴비 더미 물리 이야기는 온라인에 많고 ChatGPT가 학습 중에 이미 봤을 가능성이 큼
      그래서 이 예시는 LLM이 훈련 텍스트에서 사실상 답을 이미 본 경우를 통제하지 못한 사례처럼 보임
      영상 뒤에서 Ilya가 “존재 증명은 있다. 인간 뇌가 신경망이다”라고 말하는 부분(https://youtu.be/Gg-w_n9NJIE?t=4966)도 흥미로움. 인간 뇌도 신경망이라는 입장에 대체로 동의하지만, 실제 뉴런은 8비트로 동작하지 않고 세포 종류·DNA·호르몬 화학 환경 등이 다르다는 반론도 많아 철학적 갈림길이 있다고 봄
    • 어떤 AI 기반 시스템 하나가 수학 증명 작성 전문가가 되면, 또 하나를 얻는 비용은 파일을 복사해 다른 클라우드 인스턴스에 띄우는 정도임
      몇 분에서 몇 시간 안에 가능함
      반면 인간 전문가 하나를 더 얻으려면 수학을 직업으로 좋아하는 사람이 나타나고, 수십 년 교육과 고급 전문화를 거쳐야 하며, 그 사람이 끝까지 해내고 지식의 최전선을 밀어붙일 수준이 될 보장도 없음
      그 시간을 기다리는 동안 병렬로 작동하는 AI 전문가를 수조 개 만들 수도 있음
      인간 뇌가 새 정보를 흡수하는 대역폭은 낮지만, 기계는 평생 지식을 몇 초 만에 복제하고, 수천 개 대화를 병렬로 하며, 뇌의 일부를 직렬화해 다른 AI에 보낼 수도 있음. 프로그래머블 물질까지 도달하면 computronium을 기하급수적으로 만들고, 수천 년치 연구를 몇 초에 하는 식의 오메가 포인트도 가능해짐
    • “도우미, 사실 확인자, 지루한 일 처리자” 중에서 사실 확인자는 나머지와 성격이 다름

  • 수학은 전혀 모르지만, 소프트웨어 역사를 떠올리게 됨. 예전에는 RollerCoaster Tycoon 같은 놀라운 프로젝트가 거의 한 사람이 만든 작품이었음
    이후 소프트웨어 공학이 인터뷰에서 묘사된 것과 비슷하게 모듈화되었고, 지금은 나 같은 사람들이 생업으로 React를 찍어내는 거대한 조립라인이 되었으며 개인당 생산성이나 요구되는 실력은 거의 0에 가까워진 듯함
    분야가 전성기일 때는 천재 한 명이 머릿속에 백 가지를 담고 최고의 작업을 해내고, 그것이 조립라인으로 대체되면 그 분야는 진짜 가치 있는 것을 더 이상 만들지 못하게 된다는 인상을 받음

    • 그 직감은 인간의 본질적 힘, 즉 우리가 단순한 개인이 아니라 함께 일해 개인보다 더 큰 일을 할 수 있다는 점을 부정함
      소프트웨어 공학은 멋진 일을 멈추지 않았고, 오히려 정반대라고 봄
    • 더 몰입감 있는 일을 원하면 급여를 낮추고 스타트업에 가면 됨. 거기서는 똑같이 게으르고 정리 안 된 사람들이 더 “권위 있어 보이는” 언어로 더 엉망인 코드를 써놓았을 가능성이 큼
      농담은 제쳐두고, 언젠가 치명적 버그를 고쳐야 할 때가 오면 실력이 드러남. 제품이나 서비스가 안정적이고 수익성이 생겼다고 해서 원 개발자들이 떠났거나 누군가가 큰일을 해낼 수 없다는 뜻은 아님
    • 그 평가는 불공평함. RollerCoaster Tycoon 같은 오래된 프로젝트의 1인당 생산성은 인상적이지만, 전체 결과물은 현대 게임과 비교하면 초라함
      이 분야가 진짜 가치 있는 것을 더 이상 만들지 않는다는 말은 매우 틀렸음
      100명이 100년에 걸쳐 만든 성당과, 한 사람이 한 달 만에 만든 오두막을 비교하는 느낌임. 오두막도 서 있고 살 곳은 주지만 성당은 아님
    • 소프트웨어의 전문화와 산업화가 극단적인 모듈화와 세분화를 낳았다고 생각함
      웹 개발 쪽은 Python만 보려고 해도 바퀴의 작은 톱니마다 프레임워크와 기술이 너무 많아 따라가기가 정말 어려움
    • 대체로 동의함. “내 React 앱도 나한테는 어렵고 도전적이다”에 집착하는 반응은 핵심을 놓친 것임
      실력은 대체로 로그정규분포를 따르므로 예외적인 사람은 원래 적고, 초기의 작은 분야는 지원 인프라가 부족해 극단적 재능을 가진 사람만 살아남으면서 정상급 인재 밀도가 비현실적으로 높아질 수 있음
      최신 프레임워크 47개를 억지로 엮어 할 일 목록 앱을 찍어내는 것과 의미 있는 영향을 만드는 것은 근본적으로 다른 일임
      비용 대비 이익 관점에서는 큰일에 장기 투자하기보다 싸게 많은 코드를 뿜어내는 쪽에 강한 국소 최적점이 있고, 분야가 성숙할수록 그 지점에 도달하는 실력 하한선은 낮아짐
      정상급 인재를 훈련하는 데 집중하는 조직도 많지 않음. 그래서 분야가 커질수록 평균 실력이 방치 상태에서 떨어지는 현상은 설명하기 쉽고, 분포를 잘못 다루면 나중에 고치기 비쌀 수 있음

  • 컴퓨터 검증 증명은 AI가 꽤 가까운 시일 안에 유용해질 수 있는 영역임. 다만 완전한 LLM보다는 체스 엔진의 신경망에 더 가까울 수 있음
    모든 걸 손으로 증명하는 건 지루하고 시간이 오래 걸려 이미 많은 솔버를 쓰지만, 전술이나 솔버는 정리와 보조정리를 너무 많이 던지면 힘들어함
    관련 보조정리를 패턴 매칭해 찾는 탐색 기계로서의 신경망은 잘 맞음
    귀납법과 고차 단일화도 사실상 코드 합성이며, 가능한 모든 구문 트리를 무차별 반복하는 건 매우 비효율적임
    솔버는 어차피 백트래킹을 하므로 AI가 95% 쓸모없는 보조정리를 내도 괜찮고, 수동 검색보다 극적으로 나아질 수 있음
    다만 컴퓨터 검증 증명이 의사소통에 반드시 좋은지는 확신이 없음. 사람이 읽는 증명이 분량 말고도 여러 이유로 고수준이며 세부를 생략하는 것임

    • 수학자는 아니지만 증명 검사기가 어떻게 작동하는지 보면, 큰 미래 발전 없이는 실용화되기 어렵다고 봄. 지금은 확실히 아님
      핵심 문제는 증명에서 사용하는 수학적 대상의 형식적 정의와 연결되어야 한다는 점임
      하지만 사람은 증명을 쓰거나 읽을 때 그렇게 생각하지 않음. 보통 자신이 “도덕적으로” 무엇을 하는지에 대한 고수준의 비형식적 감각이 있고, 필요한 만큼 형식적 세부를 채움
      컴퓨터 코드는 언어의 형식 의미론이 정신 모델과 훨씬 가까워 어느 정도 작동하지만, 수학은 일반적으로 목표가 다름
    • 자동 정리 증명은 이미 오래전부터 있던 개념임
      Isabelle의 sledgehammer 전략은 E, Z3, SPASS, Vampire 같은 자동 정리 증명기를 결합해 목표를 증명하거나 반박하려고 시도함
      이론상 괜찮아 보이지만 실제로는 임의로 보이는 보조정리 12개를 적용한 재구성 증명이 나오고, 이런 증명은 읽을 수 없고 매우 취약함
      AI가 이 문제를 마법처럼 해결할 것 같지는 않음
    • 맞음. 다만 표본 효율성에서 큰 진전이 필요함
      현재 신경망은 표본 효율이 극히 낮고, 형식 수학 데이터셋은 Python 코드 같은 데이터셋보다 훨씬 작음

  • Terence Tao가 몇 달 전 이 주제로 훌륭한 강연을 했고, Lean 활용을 더 자세히 다룸: https://www.youtube.com/watch?v=AayZuuDDKP0

  • 한 현직 수학자가 연구 중 GPT-4o로 아마도 새로운 보조정리를 증명하게 했다고 함
    “내 파트너는 수학자인데, 지난주 처음으로 ChatGPT를 써서 연구용 보조정리 몇 개를 증명해 봤다. 이미 그 정리들이 참일 거라고 의심했고 접근법도 대략 있었지만, 그런 유형의 명제 전문가는 아니었다. 모델에서 정확하고 유용한 증명을 얻은 건 이번이 처음이었다
    첫 번째 보조정리는 협업자가 작은 e 값에 대한 계산에서 발견한 것이다. ChatGPT는 뫼비우스 함수를 써보라고 알려주기 전에는 증명을 찾지 못했다
    https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
    두 번째는 좀 더 표준적으로 보이고 Mathematica도 할 수 있었을 것 같다. 하지만 Mathematica는 깔끔한 유도를 주지 않으니 여전히 유용하다
    https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...”

    • Ben Goertzel이 최근 인터뷰에서 자신과 동료가 만든 새로운 수학 아이디어를 두고 GPT-4와 박사급 토론을 했다고 말함
      이런 것들은 추론과 무거운 주제에서 무서울 정도로 좋아지고 있음
      기계학습 분야가 LLM의 대체로 시스템 1 사고를 보완할 시스템 2 능력을 더하는 데 계속 집중하면 상황이 거칠어질 듯함
    • 두 번째 증명은 어떤 책이나 전자책 어딘가에 있을 가능성이 꽤 높아 보임. 떠오른 건 generatingfunctionology였음
      인상적인 기억력이지, 새로운 추론은 아님
    • 인용 출처가 궁금함. 첫 번째는 최근 친구 Beren과 얘기하던 것과 비슷해서 흥미로움
      우리는 |τ|! 계수를 가진 분할 합이 아니라 순서 있는 분할의 합으로 생각했지만, 둘은 당연히 같은 것임
      순환적으로 순서가 있는 분할, 즉 |τ|! 대신 (|τ|-1)! 계수를 쓰면 (-1)^e가 아니라 0이 나옴
      Beren의 조합론적 증명은 특별한 원소를 하나 고르고, 그 원소가 혼자 있으면 다음 부분과 합치고 혼자가 아니면 자신만의 부분으로 쪼개는 방식으로 짝수 길이와 홀수 길이의 순환 순서 분할 사이 전단사를 만드는 것임
      선형 순서의 경우 비슷하게 마지막 원소부터 적용하되, 마지막 원소가 마지막 부분에서 혼자 있는 분할은 매칭되지 않으므로 그다음 원소로 재귀적으로 진행함
      결국 모든 것이 매칭되고, 모든 원소가 따로 있으며 원래 순서대로 있는 분할만 남음. 원래 집합 크기의 짝홀에 따라 부호 합이 원래 명제로 이어짐
    • 두 번째 증명은 정말 매끈함. 왜 성립하는지 대수적 증명 말고 조합론적 증명이 있는지 궁금함
    • 첫 번째 예시에서 ChatGPT는 그냥 말이 안 되는 출력을 냈음. 6단계의 τ ≤ τ에 대한 합을 보면 τ가 합의 묶인 변수인지 자유 변수인지 불명확함
      “τ ≤ τ”에 대한 합에 항이 몇 개인지도 모르겠고, 이것이 3번의 좌변이나 우변 중 하나를 세운 뒤 다른 쪽을 결론내리는 것과 어떻게 연결되는지도 맞지 않음
      실제로는 ChatGPT가 분할 격자의 뫼비우스 함수를 기억해내서 증명 없이 되뇌고, 그 뒤에는 겉보기만 그럴듯한 헛소리를 뱉은 것임
      그 뫼비우스 함수를 세우는 것이 사실상 핵심인데, 질문은 거의 그 함수가 그런 형태임을 증명하라는 것과 같음
      게다가 ChatGPT가 내놓은 일반 공식도 약간 틀렸고, 현재 증명에 중요한 |σ| = 1인 경우에만 맞음
      이 사실은 뫼비우스 함수 전체 장치를 명시적으로 쓰지 않고도 N(t,e)를 t개 동치류로 나누는 분할 수로 두고, N(t,e+1)=N(t-1,e)+tN(t,e)라는 점화식으로 초등적 귀납을 하면 바로 보일 수 있음

  • 이 인터뷰에서 세 가지가 두드러짐
    첫째, Tao는 수학적 통찰도 사회의 다른 산출물처럼 “생산”되는 미래를 그리며 project manager mathematicians를 말함. 수학이 아직 그렇게 산업화되지 못한 이유를 도구 부족에서 찾고, AI와 증명 보조기가 이 부분에서 혁명적일 수 있다고 봄. 다만 인간의 상호작용과 안내는 여전히 필요함
    둘째, 논문에 담기지 않는 암묵지가 매우 많음. 직관이나 실패의 지식 같은 것은 중요해서, 최고 수학자들도 같은 실수를 반복하지 않으려면 서로 이야기해야 함
    셋째, 수학은 이미 충분히 형식화되어 있다고 생각하기 쉽지만 논문에는 공통 지식이 많이 전제됨. 증명 보조기가 이해할 수 있는 방식으로 증명을 형식화하면 더 많은 사람이 실제로 무슨 일이 일어나는지 이해하는 데 도움이 됨
    Tao가 Polymath 프로젝트 강연에서 보여줬듯, 그는 항상 수학 연구의 새로운 방법을 찾는 사람이라는 점이 드러남

  • 당장은 Tao나 Scholze 같은 Fields 메달리스트들이 증명에 10배 시간을 쓸 여유가 있을 때 가능한 프로젝트일 수 있음
    최근 최상위권 수학과 박사후연구원과 이야기했는데, 자기 주변에 실제 작업에서 lean4를 쓰는 사람은 없다고 했음
    경력 초반 연구자라면 직관을 믿고 논문을 내는 편이 아마 더 나을 것임

    • 수학 교수이고, Lean을 쓰거나 기여하는 사람들을 많이 알고 있음. 그들이 모두 Fields 메달리스트는 아님
      이 주제를 제대로 보려면 몇 사람의 인상만으로는 부족함
    • 수학 안에서도 분야에 따라 크게 다를 것임. 수리논리나 대수학은 원래 형식적 스타일이 강해서 증명을 Lean으로 옮기는 부담이 상대적으로 작음
      반면 저차원 위상수학처럼 더 직관적 스타일인 분야는 증명 검사기를 쓰는 사람이 적을 것으로 예상함
      여기서 직관적이라는 말은 덜 엄밀하다는 뜻이 아님. 어떤 호모토피 동치에 대한 그림 증명은 부등식 나열보다 Lean이 이해할 수 있게 옮기기 훨씬 어려움
      참고로 기하/위상 쪽에 있는데, 아직 이런 도구를 쓰는 사람을 보거나 들은 적은 없음
    • Tao에게 증명에 10배 시간을 쓴다는 건 여전히 평균적인 박사후연구원보다 5배 적은 시간을 쓴다는 뜻일 수 있음. 그는 믿기 어려울 만큼 빠르고 생산적임
    • lean4는 프로그래밍 언어이자 정리 증명기임
      https://lean-lang.org/
      https://github.com/leanprover/lean4

  • “AI가 이해 불가능하고 못생긴 증명을 제공하면, 그걸 가지고 분석할 수 있다. 이 증명이 10개 가정을 써서 하나의 결론을 얻는다면, 가정 하나를 지워도 증명이 여전히 동작하는가? 이런 과학은 아직 AI 생성 증명이 많지 않아 존재하지 않지만, AI 생성 수학을 받아 더 이해 가능하게 만드는 새로운 유형의 수학자가 생길 것이다”라는 부분이 코드의 공개 API 설계에 대한 내 생각과 정확히 같음
    전통적으로 숙련 개발자만 하던 역할이 이제 크게 단순화되어 모두에게 접근 가능해질 수 있음

답변달기