Claude가 11일 만에 페르마 정리를 증명했습니다. 평가: SHIP IT.

이 동영상에서 다루는 내용

• Claude는 Lean 4에서 페르마 마지막 정리를 형식화합니다.
• Chromium 샌드박스 RCE (CVE-2026-85046), 실제 악용됨, 1,000달러 현상금
• 신진서가 카타고를 두 점 접바둑으로 이겼습니다.

번역된 스크립트

원래 영어 내레이션에서 번역되었습니다. 사용 가능한 오디오 및 캡션은 YouTube에서 제어합니다.

0:00 페르마는 그의 놀라운 증명이 여백에 들어가지 않을 것이라고 말했고, 오늘 Anthropic은 여백을 공개했습니다: 1300만 줄의 Lean, Mathlib 크기의 5배이며, 모든 수학자들이 이미 믿고 있던 정리를 증명했습니다. Anthropic이 게시했을 때 트빌리시는 밤 10시에서 11시 사이였고, 그래서 당연히 저는 깨어 있었습니다. 어제 Google은 12개의 보안 수정 사항이 포함된 Chrome 152를 출시했으며, 그중 하나는 이미 실제 악용된 V8 버그였고, 제보자에게는 1000달러를 지급했습니다. 이는 나중에 언급할 세단보다 적은 금액입니다.

0:26 또한 어제 Mullvad는 11월 2일에 공개 암호화 DNS를 종료하고 대신 Quad9에 비용을 지불할 것이라고 밝혔으며, 오늘 아침 Rust React 컴파일러는 Vite에서 네이티브로 실행되었고, Hacker News는 IBM Bob, AI 코딩 에이전트를 발견했습니다. 그리고 Claude가 페르마 마지막 정리를 형식화했고, 같은 첫 페이지에서 한국의 그랜드마스터가 지구상에서 가장 강한 바둑 엔진을 이겼으므로, 오늘 인류는 두 번 시도하여 한 번 성공했습니다. 이 영상에서: Claude가 실제로 증명한 것, 그 비용,

0:52 이것에 평생을 바친 수학자가 이것이 아무것도 바꾸지 않는다고 말하면서도 여전히 기뻐하는 이유, 그리고 인간이 바둑에서 기계를 어떻게 이겼는지. 9월 4일 금요일, The Daily Diff입니다. 페르마 마지막 정리: 2보다 큰 어떤 n에 대해서도 양의 정수 a, b, c는 a의 n승 + b의 n승 = c의 n승을 만족하지 않습니다. 페르마는 1637년경 여백에 그것을 휘갈겨 쓰고 그의 작업을 보여주지 않고 죽었으며, 그로 인해 그는 '내 컴퓨터에서는 잘 됩니다'로 티켓을 닫은 최초의 개발자가 되었습니다. 1908년 10만 골드 마르크 상금은 첫해에 621개의 틀린

1:25 증명을 끌어들였고, 앤드루 와일즈는 마침내 1995년에 성공했습니다. 심사관들이 검증하는 데 몇 달이 걸린 129페이지였습니다. 형식화는 그 증명을 Lean이라는 증명 보조 도우미가 모든 단계를 기계적으로 확인할 수 있도록 다시 작성하는 것을 의미하며, 임페리얼의 케빈 버자드는 2024년부터 정확히 그 일을 하기 위한 인간의 노력을 이끌었습니다. 청사진만 86 페이지에 달합니다. 대신 Anthropic 연구원 펑 톈이는 수십 명의 Claude 에이전트를 Prove2Me라는 플랫폼에 투입했으며, 이 플랫폼은 정리 명제의 DAG를 유지하여 에이전트들이 다음에 무엇을 증명할지 알 수 있도록 합니다. 왜냐하면 이것 없이는 첫 번째

2:00 swarm들이 누가 무엇을 증명하고 있는지 놓쳤기 때문입니다. 이는 오케스트레이션 레이어가 마케팅 예산을 가진 정규 표현식일 때 일어나는 일입니다. 11일 후 루트 노드는 '증명됨'으로 표시되었습니다: 1300만 줄의 Lean, 29,500개의 중간 정리, 내부 모델에서 약 60억 개의 출력 토큰. 이는 Claude Fable 5.1과 대략 비슷합니다. 증명이 Lean의 세 가지 표준 공리에 정확히 기반하지 않으면 빌드가 실패합니다. 죄송합니다, 네이티브 decide도 없고, 속임수도 없습니다. 검사 비용도 저렴하지 않습니다: 처음부터 빌드하는 데

2:29 96개 코어와 153기가바이트의 RAM으로 5시간 반이 걸렸고, 정리 이름은 기계 생성된 것이므로, 저장소는 '읽기보다는 검사하기 위해 작성되었다'고 스스로 설명합니다. 이것은 제가 엔터프라이즈 자바를 설명하는 방식과도 같습니다. 이제 모순입니다. Anthropic의 게시물은 Lean이 의심할 여지 없이 정확성을 입증한다고 말합니다. 케빈 버자드, 이 일에서 뒤처진 사람은 Anthropic이 빌려준 500기가바이트 머신에서 저장소를 컴파일하고, 검증되었음을 확인한 다음 이렇게 썼습니다. 인용하자면, '수학적으로 이 작업은 본질적으로 아무것도 알려주지 않습니다.'

2:56 그는 이미 정리가 참이라고 99.9% 확신했으며, 이 증명은 새로운 수학을 추가하지 않습니다. 이것이 보여주는 것은 자동 형식화가 현재 무엇을 할 수 있는지이며, 그 부분에 대해 그는 진정으로 기뻐하고 있습니다. 그는 5년 동안 100만 파운드를 받았지만, Anthropic은 11일이 걸렸고, 한 댓글 작성자의 어림짐작에 따르면 60억 개의 출력 토큰은 정가로 한 댓글 작성자의 어림짐작에 따르면 60억 개의 출력 토큰은 정가로 상당한 비용이 듭니다. 약 30만 달러 정도였으므로 기계가 더 저렴했습니다. 기계 훈련 비용은 아무도 계산하지 않으므로 제외하고요.

3:24 가장 중요한 부분: 그가 웨일스의 음악 축제에 있을 때 이메일이 도착했는데, 4G 신호가 한 칸밖에 없는 상태에서 한 번도 들어본 적 없는 이름으로 온 이메일이라 그는 장난인 줄 알고 무시했습니다. 그리고 일주일 후에 읽었는데, 이는 다음을 포함하는 모든 제목에 대한 올바른 반응입니다. 종단 간 공식화. 한편, 인간은 한 골을 만회했습니다. 세계 바둑 랭킹 1위 신진서 9단은 카타고를 꺾었습니다. 가장 강력한 오픈 소스 바둑 엔진인 카타고를 상대로 서울에서 두 점 접바둑으로 2승 1패를 거두었습니다. 이는 최고 프로 기사와 신인 프로 기사 사이의 격차와 거의 같습니다.

3:50 결정적인 대국은 221수 만에 11.5점 차로 승리했으며, 중반부터 99%의 승리 확률을 유지했고, 2억 5천만 원(약 17만 달러)과 제네시스 G90을 받았습니다. 따라서 초인적인 AI를 물리친 보상은 크롬 샌드박스 탈출에 대한 구글의 현상금보다 170배 많습니다. 그의 설명: 초반에는 AI의 수를 모방하다가 패배했습니다. 그는 자신만의 스타일로 바둑판을 만들며 승리했습니다. 이는 올해 제가 들은 AI에 대한 가장 유용한 조언이며, 보드 게임에서 나온 것입니다. 올해 제가 들은 AI에 대한 가장 유용한 조언이며, 보드 게임에서 나온 것입니다. 차이점에 두 줄 더 있습니다.

4:22 oxc의 Rust React 컴파일러가 이제 하나의 플래그 뒤에 Vite에 내장됩니다. 1,036개 파일의 코드베이스는 컴파일 단계에서 14.3초에서 0.81초로 단축되었으며, 주로 package.json에서 Babel을 삭제함으로써 이루어졌습니다. 이는 제 피부 관리 루틴이기도 합니다. 주로 package.json에서 Babel을 삭제함으로써 이루어졌습니다. 이는 제 피부 관리 루틴이기도 합니다. 그리고 IBM은 "안녕하세요, 저는 밥입니다"라고 인사하고 하위 에이전트를 생성하며 메인프레임 코드를 현대화하는 AI 코딩 파트너 Bob을 출시했습니다. 저는 Bob입니다'라고 인사하고, 서브 에이전트를 생성하고, 메인프레임 코드를 현대화하며, Bobalytics라는 분석 제품을 출시했습니다. 그래서 어딘가의 은행은 매우 흥분했고 아무도 라이선스를 읽지 않았습니다.

4:51 한 금요일에 너무 많은 마진이 있었습니다. 이 내용을 제가 말하는 것보다 읽고 싶다면, 매일 아침 차이점이 사서함으로 도착합니다 — daily diff dot에서 무료입니다. 말하는 것보다 읽고 싶다면, 매일 아침 차이점이 사서함으로 도착합니다. daily diff dot dev, 아래 링크. 그래서, 오늘의 판결: SHIP IT. 커널은 찬성하고, 버자드는 찬성하며, 수학은 변하지 않았지만, 수학을 확인하는 방식은 방금 바뀌었습니다. 그게 오늘의 차이점입니다. 저는 Axrisi의 Niko입니다.

5:09 책임감 있게 병합하세요.

출처

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com