#Lean
3개의 포스트
![[특집] 수학의 미래 — 타오의 블로그에 실린 아비가드의 편지: '더 어려운 문제를 풀고, 더 큰 생각을 하고, 새로운 것을 시도하라'](/_next/image?url=https%3A%2F%2Ffiles.core.today%2Fstorage%2Fcoredot%2Fpublic%2Fblog%2Ffom-cover.webp&w=3840&q=75)
[특집] 수학의 미래 — 타오의 블로그에 실린 아비가드의 편지: '더 어려운 문제를 풀고, 더 큰 생각을 하고, 새로운 것을 시도하라'
2026년 10월 5일, 테런스 타오의 블로그에 카네기멜런 대학의 논리학자이자 Lean 수학 라이브러리의 산파인 제러미 아비가드의 글 「수학의 미래」가 실렸다. 한 달 내내 경고와 선언이 쏟아지던 블로그에 처음으로 '대체로 긍정적'이라는 진단과 함께 세 개의 동사가 나왔다 — 더 어려운 문제를 풀어라, 더 큰 생각을 하라, 새로운 것을 시도하라. 그리고 다음 세대에게 '우리는 당신들과 함께 선다'는 문장이 붙었다. 이 글은 왜 화제가 됐는가. 리만의 1854년 강연을 '어떤 강화학습 채점기도 평가할 수 없었을 것'이라고 한 기술적 주장은 무슨 뜻인가. 추론 모델이 실제로 어떻게 훈련되는지(GRPO·결과 보상·AlphaProof의 탐색 트리)부터, 수학이 '낯선 기술'을 삼켜 온 400년의 역사, 댓글창의 반론, 같은 주에 바뀐 arXiv·Erdős 사이트의 규칙, 그리고 2026년 한국의 자리까지, 원문과 논문·댓글 100여 건을 읽고 인터랙티브 다섯 개와 함께 풀어본다.
![[특집] 722편의 원고 — OpenAI가 하룻밤에 공개한 372개의 '해결된' 수학 문제, 그 저장소를 열어 보다](/_next/image?url=https%3A%2F%2Ffiles.core.today%2Fstorage%2Fcoredot%2Fpublic%2Fblog%2Foam-cover.webp&w=3840&q=75)
[특집] 722편의 원고 — OpenAI가 하룻밤에 공개한 372개의 '해결된' 수학 문제, 그 저장소를 열어 보다
2026년 10월 6일 밤, OpenAI는 일곱 문단짜리 글 「수학에서의 AI 진전을 공유합니다」와 함께 GitHub 저장소 하나를 열었다. 미공개 내부 모델이 쓴 수학 원고 722편, 결과 계열 372개. 준(準) 리만 가설, 4차원 카케야 추측, 행렬 곱셈 지수 2.25, 유일 게임 추측, 톰프슨 군 F의 비순종성 — 각각이 사람이 했다면 경력을 통째로 바칠 만한 문제들이 '거의 전부 프롬프트 하나, 에이전트 하나, 평균 세 시간'으로 나왔다고 적혀 있다. 이 글은 저장소를 직접 열어 README·카탈로그·Lean 라이브러리·추론 요약 10건을 읽고, 헤드라인 결과를 비전공자도 이해할 수 있게 풀고, '검증됨'과 '이해됨' 사이의 거리를 재고, 사흘간 쏟아진 수학자들의 반응('즉시 필즈상'에서 '힘의 시연'까지)을 지도에 놓는다. 그리고 하루 전 같은 블로그에 실린 아비가드의 편지와 겹쳐 읽는다.
페르마의 마지막 정리, AI가 11일 만에 '형식 증명'하다 — 350년의 여백, 1,300만 줄의 Lean, 그리고 수학 검증의 미래
2026년 9월 4일 Anthropic이 '컴퓨터가 검증한 최초의 페르마의 마지막 정리 증명'을 공개했다. Claude 에이전트 수십 개가 11일 동안 1,300만 줄의 Lean 코드를 쓰고 29,511개의 중간 정리를 증명했다. 1637년의 여백에서 1995년 와일스의 129쪽, 그리고 2026년의 의존 그래프까지 — 왜 '증명을 검증하는 일'이 이렇게 어려웠는지, 형식화가 무엇인지, Prove2Me 아키텍처가 어떻게 수십 개 에이전트를 협업시켰는지, 그리고 이 증명이 정직하게 무엇을 못 했는지까지 사례와 그림으로 풀어본다.