#형식 검증
3개의 포스트
![[특집] 수학자가 훨씬 더 많이 필요해질 것이다 — AI가 아이디어를 쏟아낼 때, '이해'는 누가 하는가](/_next/image?url=https%3A%2F%2Ffiles.core.today%2Fstorage%2Fcoredot%2Fpublic%2Fblog%2Fnm-cover.webp&w=3840&q=75)
[특집] 수학자가 훨씬 더 많이 필요해질 것이다 — AI가 아이디어를 쏟아낼 때, '이해'는 누가 하는가
2026년 9월 24일, 테런스 타오의 블로그에 암호학자 아밋 사하이의 짧은 글이 실렸습니다. 제목은 「수학자가 훨씬 더 많이 필요해질 것이다」. AI가 사람이 따라가지 못할 속도로 아름다운 아이디어를 내놓기 시작한 지금, 수학자들이 '이해하는 일'을 포기한다면 그것은 인류에 대한 책임을 내려놓는 일이라는 주장입니다. 이 특집은 그 글을 뼈대로, 1970년대 서스턴이 한 분야를 '청소해 버린' 이야기부터 페렐만의 68쪽을 세 팀이 수백 쪽으로 풀어낸 일, 14년째 아무도 합의하지 못한 모치즈키의 증명까지 '증명과 이해 사이의 시차'를 따라갑니다. '정리는 모델 안에서만 존재한다'는 문장을 암호학과 공학 사고로 풀어 보고, AI가 설계한 1테라와트 핵융합 발전소라는 사고실험을 공청회 퀴즈로 직접 겪어 봅니다. 사람이 끼면 오히려 결과가 나빠진다는 실험 106개의 메타분석, 2차 세계대전의 수학자 동원에서 찾은 '지적 예비군'의 선례, 그리고 일자리를 걱정하는 젊은 연구자들의 반론까지 — 인터랙티브 6개와 웹툰 12장으로 함께 읽어 보세요.
AI와 수학의 심각한 불일치 — 필즈상 수상자 25인은 무엇을 두려워하는가: 등대, 파이프라인, 그리고 나비에–스토크스 88시간
2026년 9월 11일, 테런스 타오·페터 숄체·마리나 비아조우스카 등 필즈상 수상자 25명이 'AI와 수학의 심각한 불일치'라는 선언을 냈다. AI 기업이 유명 미해결 문제를 벤치마크 삼아 푸는 경쟁이 수학이라는 학문과 공동체에 해롭다는 것이다. 이 선언은 어디서 왔는가. OpenAI가 1만 개 에이전트로 88시간 만에 '풀었다'고 발표한 나비에–스토크스 문제, 그 직전에 같은 문제를 1년간 파던 두 수학자의 4쪽짜리 성명, '10년간 진전 없음'이라는 문구에 항의한 독일 수학자의 이메일, 타오가 ICM에서 그린 다섯 단계 파이프라인과 굿하트의 법칙까지 — 왜 '문제를 푸는 것'과 '수학을 하는 것'이 갈라졌는지를 논문·선언문·논쟁 100건을 읽고 인터랙티브와 함께 풀어본다.
페르마의 마지막 정리, AI가 11일 만에 '형식 증명'하다 — 350년의 여백, 1,300만 줄의 Lean, 그리고 수학 검증의 미래
2026년 9월 4일 Anthropic이 '컴퓨터가 검증한 최초의 페르마의 마지막 정리 증명'을 공개했다. Claude 에이전트 수십 개가 11일 동안 1,300만 줄의 Lean 코드를 쓰고 29,511개의 중간 정리를 증명했다. 1637년의 여백에서 1995년 와일스의 129쪽, 그리고 2026년의 의존 그래프까지 — 왜 '증명을 검증하는 일'이 이렇게 어려웠는지, 형식화가 무엇인지, Prove2Me 아키텍처가 어떻게 수십 개 에이전트를 협업시켰는지, 그리고 이 증명이 정직하게 무엇을 못 했는지까지 사례와 그림으로 풀어본다.