# 에르되시 문제 웹사이트에서 AI 지원이 일상화되는 중 > Clean Markdown view of GeekNews topic #24583. Use the original source for factual precision when an external source URL is present. ## Metadata - GeekNews HTML: [https://news.hada.io/topic?id=24583](https://news.hada.io/topic?id=24583) - GeekNews Markdown: [https://news.hada.io/topic/24583.md](https://news.hada.io/topic/24583.md) - Type: GN+ - Author: [neo](https://news.hada.io/@neo) - Published: 2025-11-25T04:35:34+09:00 - Updated: 2025-11-25T04:35:34+09:00 - Original source: [mathstodon.xyz](https://mathstodon.xyz/@tao/115591487350860999) - Points: 1 - Comments: 1 ## Topic Body - **에르되시 문제 #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 대화의 정확도 문제를 언급하며, **세밀한 조정이 필요하지만 사용이 즐겁다**고 평가함 ## Comments ### Comment 46740 - Author: neo - Created: 2025-11-25T04:35:35+09:00 - Points: 1 ###### [Hacker News 의견](https://news.ycombinator.com/item?id=46017972) - 수학 중심의 **ML 논문**을 AI 어시스턴트에게 던져서 간단한 설명이나 의사코드로 돌려받을 수 있다는 게 놀라운 경험임 대학에서 배운 걸 25년 넘게 써본 적 없던 나로서는 정말 큰 도움임 - 그 설명이 정확한지 어떻게 검증하는지 궁금함. 수학적 정의는 아주 미묘한 부분이 많음 - 이런 점이야말로 LLM이 학습에 빛을 발하는 부분이라 생각함 논문을 Claude에 넣고 개요를 받은 뒤 질문을 이어갈 수 있음 내가 학사나 석사 때 배우지 않았던 **생물학** 같은 분야에서도, 지식 있는 튜터와 대화하듯 깊이 파고들 수 있었음 - 수학 표기법은 **맥락 의존성**이 높아서, LLM에게 Lisp 같은 저맥락 언어로 변환해달라고 하면 훨씬 빠르게 구조를 파악할 수 있음 - 연구자와 기업이 과학적 연구에서 더 많은 **생산성 향상**을 얻기를 바람 완벽하지 않은 어시스턴트라도 충분히 레버리지를 높여줌 - Tao가 언급한 iOS용 **형식화 앱** 베타 버전이 있음 → [Aristotle](https://aristotle.harmonic.fun/) 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](https://en.wikipedia.org/wiki/DR-DOS)의 후속작처럼 느껴짐 - 실제로 **AI 통합 IDE**인 [Erdos](https://www.lotas.ai/erdos)라는 제품이 존재함 - 그는 기존의 **프런티어 도구**를 잘 활용해 협업적인 수학 연구 환경을 만들어낸 점이 인상적임 - 다행히 수학은 **우상화나 인기 경쟁**이 결과의 진위를 결정하지 않는 분야임 이런 이유로 수학은 여전히 **사이비적 영향력에서 자유로운 드문 학문**이라 생각함