#수학
7개의 포스트
![[특집] 기계가 질문을 만들 때 — 가우스의 소수표에서 AlphaEvolve까지, '추측 기계' 50년사](/_next/image?url=https%3A%2F%2Ffiles.core.today%2Fstorage%2Fcoredot%2Fpublic%2Fblog%2Fcjm-hero.webp&w=3840&q=75)
[특집] 기계가 질문을 만들 때 — 가우스의 소수표에서 AlphaEvolve까지, '추측 기계' 50년사
3Blue1Brown 영상이 '두 번째 시나리오'로 남겨 둔 질문 — 기계가 좋은 질문까지 던지게 되면? — 은 사실 50년 된 연구 분야다. 레넛의 AM, 벽에 추측을 쓰던 Graffiti, 연분수를 쏟아내는 라마누잔 머신, 사람의 직관을 안내한 딥마인드의 매듭 연구, 프로그램을 진화시키는 FunSearch와 AlphaEvolve까지. 생성·검증·선별이라는 세 역할로 각 시스템의 구조를 해부하고, 브라우저에서 직접 추측 기계를 돌려 본다.
![[특집] 수학의 두 문화 — 재프–퀸, 서스턴, 고워스를 정독하고 AI가 쓴 수학의 '문화'를 재다](/_next/image?url=https%3A%2F%2Ffiles.core.today%2Fstorage%2Fcoredot%2Fpublic%2Fblog%2Ftcm-hero.webp&w=3840&q=75)
[특집] 수학의 두 문화 — 재프–퀸, 서스턴, 고워스를 정독하고 AI가 쓴 수학의 '문화'를 재다
1993년 재프와 퀸은 '증명 없는 사변'이 수학을 망칠 수 있다고 경고했고, 1994년 서스턴은 수학의 생산물은 정리가 아니라 이해라고 답했다. 2000년 고워스는 문제를 푸는 문화와 이론을 짓는 문화를 나눴다. 30년 묵은 이 논쟁을 원문으로 정독하고, 2026년 OpenAI가 공개한 AI 수학 원고 수백 편과 사람이 쓴 arXiv 논문의 초록을 고워스의 두 문화로 분류해 기계가 어느 문화에 서 있는지 직접 쟀다.
![[특집] AI가 쓴 증명은 누가 소화하나 — 타오의 '증명 소화불량'과 해설 실측](/_next/image?url=https%3A%2F%2Ffiles.core.today%2Fstorage%2Fcoredot%2Fpublic%2Fblog%2Fpdx-hero.webp&w=3840&q=75)
[특집] AI가 쓴 증명은 누가 소화하나 — 타오의 '증명 소화불량'과 해설 실측
기계가 증명을 만들고 Lean이 검증까지 끝냈는데, 문제는 여전히 '열림(open)'이다. 아무도 그 증명을 소화하지 못했기 때문이다. 테렌스 타오가 이름 붙인 '증명 소화불량'의 뜻과 역사, 증명을 '이해했다'를 재는 교육학의 일곱 가지 잣대를 살펴본다. 그런 다음 OpenAI가 IMO 2025에 낸 날것의 답안 다섯 편을 AI에게 세 가지 문체로 해설시키고, 원 증명을 보지 못한 '눈먼 독자' 모델에게 읽혀 이해도와 오류 탐지를 직접 쟀다.
수학은 언어다 (0편): 테런스 타오가 고른 여섯 개의 기둥, 그리고 AI 시대에 이 언어가 필요한 이유
필즈상 수학자 테런스 타오는 83분짜리 Big Think 인터뷰에서 수학 전체를 여섯 개의 기둥으로 정리했다 — 수·대수·기하·확률·해석·동역학. 그리고 이렇게 말했다. '기술적 복잡성을 벗겨내면 이것들은 극도로 직관적인 개념이고, 수학은 그것을 아주 정밀하게 기술하는 언어일 뿐이다.' 시리즈 0편에서는 왜 수학을 '언어'로 봐야 하는지, 여섯 기둥이 어떻게 과학과 기술이 되는지, 그리고 AI가 증명을 쏟아내는 2026년에 이 언어를 배우는 일이 왜 더 중요해졌는지를 다룬다.
페르마의 마지막 정리, AI가 11일 만에 '형식 증명'하다 — 350년의 여백, 1,300만 줄의 Lean, 그리고 수학 검증의 미래
2026년 9월 4일 Anthropic이 '컴퓨터가 검증한 최초의 페르마의 마지막 정리 증명'을 공개했다. Claude 에이전트 수십 개가 11일 동안 1,300만 줄의 Lean 코드를 쓰고 29,511개의 중간 정리를 증명했다. 1637년의 여백에서 1995년 와일스의 129쪽, 그리고 2026년의 의존 그래프까지 — 왜 '증명을 검증하는 일'이 이렇게 어려웠는지, 형식화가 무엇인지, Prove2Me 아키텍처가 어떻게 수십 개 에이전트를 협업시켰는지, 그리고 이 증명이 정직하게 무엇을 못 했는지까지 사례와 그림으로 풀어본다.
콜모고로프-아르놀드 정리 완전 해부 — 130년 된 수학 난제가 AI의 미래를 바꾸고 있다
1900년 힐베르트가 던진 도전장, 19세 천재 아르놀드의 증명, 그리고 2024년 MIT에서 탄생한 KAN까지 — 130년에 걸친 수학 정리가 어떻게 AI 신경망의 새로운 패러다임이 되었는지, 역사·논문·사례로 깊이 파고듭니다.
보편 근사 정리: 신경망은 정말로 아무 함수나 흉내 낼 수 있을까?
1969년 '퍼셉트론은 XOR도 못 푼다'는 선고로 AI 겨울이 시작되었다. 20년 뒤, 한 편의 논문이 반격했다 — '뉴런이 충분하면 어떤 함수든 근사할 수 있다.' 보편 근사 정리의 드라마틱한 역사를 레고 블록과 만화로 풀어본다.