▲

에르되시 문제 웹사이트에서 AI 지원이 일상화되는 중

 (mathstodon.xyz)
1P by GN⁺ 10일전 | ★ favorite | 댓글 1개
  • 에르되시 문제 #367 해결 과정에서 AI 도구가 핵심 역할을 수행하며, 인간 수학자와 협업하는 사례가 보고됨
  • Wouter van Doorn이 문제의 두 번째 부분에 대한 인간 생성 반증을 제시했고, 이후 Gemini Deepthink가 관련 합동식의 완전한 증명을 생성
  • Terence Tao가 Gemini의 p-진 대수적 수론 기반 증명을 더 단순한 형태로 변환해 게시, 이후 Lean 형식화 가능성을 언급
  • Boris Alexeev가 Harmonic의 Aristotle 도구를 이용해 Lean 형식화를 완료했으며, AI 악용 방지를 위해 최종 명제는 수동으로 검증
  • 이러한 일련의 과정은 수학 연구에서 AI 보조가 점차 표준 절차로 자리잡고 있음을 보여줌

에르되시 문제 #367의 AI 협업 사례

  • 11월 20일, Wouter van Doorn이 문제의 두 번째 부분에 대한 반증을 제시했으며, 이는 특정 합동식이 참이라는 가정에 의존함
    • 그는 해당 합동식의 타당성을 다른 참여자들이 검증해주길 요청함
  • 몇 시간 후 Terence Tao가 이 문제를 Gemini Deepthink에 제시했고, 약 10분 만에 합동식의 완전한 증명과 전체 논증 확인을 얻음
    • Gemini의 증명은 p-진 대수적 수론을 사용했으며, Tao는 이를 더 단순한 초등적 증명으로 변환해 사이트에 게시
    • Tao는 이 증명이 Lean에서 ‘vibe formalizing’ 이 가능할 것이라고 언급함

Lean 형식화 및 검증

  • 이틀 뒤 Boris Alexeev가 Harmonic의 Aristotle 도구를 사용해 Lean 형식화를 완료함
    • AI 오용을 방지하기 위해 최종 명제는 수동으로 직접 형식화
    • 전체 과정은 약 2~3시간 소요되었으며, 결과물은 온라인에 공개됨
  • Tao는 이후 AI를 이용한 문헌 검색을 수행했으나, 관련된 연구는 일부 있었지만 문제 #367과 직접 관련된 것은 발견되지 않음

커뮤니티 반응과 논의

  • 일부 사용자는 Tao의 업데이트를 통해 AI의 학문적 수학 활용 현황을 흥미롭게 지켜보고 있음
  • 다른 사용자는 Lean의 형식주의적 접근에 비판적 견해를 제시하며, 수학적 이해는 압축(compression)인데 Lean은 이를 저수준 세부로 분해(decompression) 한다고 지적
    • 관련 문서 *“Against Lean: Why Proof Assistants Formalize the Wrong Thing”*에서는 Lean과 유사한 증명 보조기가 수학의 본질을 잘못 포착하고 있다고 주장
  • 또 다른 사용자는 AI 대화의 정확도 문제를 언급하며, 세밀한 조정이 필요하지만 사용이 즐겁다고 평가함
▲
GN⁺ 10일전  [-]
Hacker News 의견

  • 수학 중심의 ML 논문을 AI 어시스턴트에게 던져서 간단한 설명이나 의사코드로 돌려받을 수 있다는 게 놀라운 경험임
    대학에서 배운 걸 25년 넘게 써본 적 없던 나로서는 정말 큰 도움임

    • 그 설명이 정확한지 어떻게 검증하는지 궁금함. 수학적 정의는 아주 미묘한 부분이 많음
    • 이런 점이야말로 LLM이 학습에 빛을 발하는 부분이라 생각함
      논문을 Claude에 넣고 개요를 받은 뒤 질문을 이어갈 수 있음
      내가 학사나 석사 때 배우지 않았던 생물학 같은 분야에서도, 지식 있는 튜터와 대화하듯 깊이 파고들 수 있었음
    • 수학 표기법은 맥락 의존성이 높아서, LLM에게 Lisp 같은 저맥락 언어로 변환해달라고 하면 훨씬 빠르게 구조를 파악할 수 있음

  • 연구자와 기업이 과학적 연구에서 더 많은 생산성 향상을 얻기를 바람
    완벽하지 않은 어시스턴트라도 충분히 레버리지를 높여줌

    • Tao가 언급한 iOS용 형식화 앱 베타 버전이 있음 → Aristotle
      Robin Hood CEO가 창업한 스타트업이라 함

  • ‘Vibe formalizing’은 ‘vibe engineering’과 ‘vibe coding’의 논리적 확장처럼 느껴짐
    문제의 조각들이 잘 안 맞을 때, 비공식적 방법과 수학적 엄밀성을 결합하는 ‘Move 37 as a Service’ 같은 접근이 흥미로움

    • 예전에 polyhedral compilation 논문을 읽다가 막혔던 부분이 있었는데, ChatGPT가 reasoning 과정을 잘 이끌어줬음
      물론 틀린 부분도 있었지만, 내 혼란을 반영해 대화하며 이해를 깊게 할 수 있었음
      AI는 사용자의 혼란 지점을 파악하는 데 특히 강함

  • 헝가리 수학자 Erdős의 이름 발음 이야기를 들었음
    헝가리어는 철자와 발음이 거의 일치하지만, 이름에서는 예외가 있음
    영어식으로는 대략 “airdish”처럼 들린다고 함

    • Ő는 단순히 œ(oe) 소리임. 헝가리 이름의 -y는 귀족 혈통을 의미하던 -i 어미의 흔적임
      예: Görgey, Széchényi, Lánczos 등
      헝가리 이름 순서는 일본처럼 성-이름(big endian) 순서임. 예: “Erdős Pál”, “Neumann János”
    • 1960년 수학과 게시판에서 본 유머시가 있었음 — Erdos가 쓴 논문이 ‘원은 둥글다’ 정리를 반박했다는 농담이었음
    • 언어마다 발음기호(발음 부호) 의 의미가 다르기 때문에, 헝가리식 부호를 영어 문장에 그대로 쓰는 건 어색하다고 생각함
    • 처음엔 “airdish” 발음이 이상했는데, ‘os’ 어미를 경구개화(palatalize) 해보니 그럴듯하게 들렸음
    • 미국인이 아니라서 그런지, 이런 발음 문제엔 아무도 신경 안 쓰는 듯함

  • 댓글 중에 anti-Lean 성향의 반응이 있다는 점이 흥미로움

    • 수학자는 아니지만, 그 반Lean 자료가 신뢰할 만한지 궁금함
      단순히 다른 접근법을 홍보하는 건지, 아니면 철학적으로 Lean에 반대하는 건지 알고 싶음
    • Tao처럼 유명한 인물은 괴짜나 음모론자들의 관심을 많이 받기 마련임

  • 연구 수학에서 AI를 써본 결과는 혼합적이었음
    비자명한 논증을 자동 완성하기도 하지만, 어떤 영역에서는 완전히 길을 잃음
    아직은 AI가 수학자를 대체하기보다는 보조 도구로서만 유용한 시점이라 생각함

    • 나도 비슷한 경험을 함. 논문에서 단순한 순열 계산 문제를 시켰는데, 직접 푸는 것보다 시간이 더 걸렸음
      코딩에서도 사소한 버그를 못 잡는 경우가 있었지만, 복잡한 작업에서는 큰 도움을 받았음
      결국 이 도구들은 전문가를 대체하기엔 아직 멀었고, 과대포장은 오히려 신뢰를 해칠 수 있음
      ‘달을 약속했다면 달을 줘야 한다’는 말처럼, 현실적인 기대치가 중요함

  • 내 생애에 ‘스타트렉’처럼 “컴퓨터, 이 수학 문제의 증명을 그려줘”라고 말할 수 있는 시대가 올 줄은 믿기지 않음
    “Beam me up Scotty”도 가능했으면 좋겠음

    • 하지만 그럴 때마다 죽을 수도 있으니, 그건 좀 곤란할 듯함

  • 오늘 밤 운전 중에 ChatGPT와 LLVM과 GCC 파이프라인 스케줄러의 세부 구조에 대해 대화했음
    덕분에 생산성이 크게 향상되었고, 실험 중인 컴파일러 관련 노트를 자동으로 정리해줬음
    예전엔 상상도 못 했던 일임

    • 내 경험상 LLM이 세부 내용 중 일부는 틀렸을 가능성이 높음
      물론 사람마다 결과는 다를 수 있음

  • AI 이름을 Erdos로 지으면, 우리 모두의 Erdos number가 1이 될 것 같음

    • 혹은 DR-DOS의 후속작처럼 느껴짐
    • 실제로 AI 통합 IDE인 Erdos라는 제품이 존재함

  • 그는 기존의 프런티어 도구를 잘 활용해 협업적인 수학 연구 환경을 만들어낸 점이 인상적임

    • 다행히 수학은 우상화나 인기 경쟁이 결과의 진위를 결정하지 않는 분야임
      이런 이유로 수학은 여전히 사이비적 영향력에서 자유로운 드문 학문이라 생각함
답변달기