Claude đã chứng minh định lý Fermat trong 11 ngày. Phán quyết: SHIP IT.

Nội dung video này đề cập

• Claude chính thức hóa Định lý cuối cùng của Fermat trong Lean 4
• Lỗ hổng Chromium sandbox RCE (CVE-2026-85046), bị khai thác trong thực tế, tiền thưởng 1.000 USD
• Shin Jin-seo đánh bại KataGo với lợi thế hai quân

Bản ghi đã dịch

Được dịch từ lời tường thuật tiếng Anh gốc. Âm thanh và phụ đề có sẵn được điều khiển bởi YouTube.

0:00 Fermat nói rằng bản chứng minh tuyệt vời của ông sẽ không vừa lề giấy, và hôm nay Anthropic đã công bố lề giấy: mười ba triệu dòng Lean, gấp năm lần kích thước của Mathlib, chứng minh một định lý mà mọi nhà toán học đã tin tưởng. Lúc Anthropic đăng bài là mười giờ kém mười một ở Tbilisi, nên tất nhiên tôi còn thức. Hôm qua Google đã ra mắt Chrome 152 với mười hai bản sửa lỗi bảo mật, một trong số đó là lỗi V8 đã bị khai thác trong thực tế, và đã trả cho người báo cáo một ngàn đô la, ít hơn chiếc sedan chúng ta sẽ nói đến sau.

0:26 Cũng hôm qua, Mullvad nói rằng họ sẽ ngừng hoạt động DNS được mã hóa công khai vào ngày 2 tháng 11 và trả tiền cho Quad9 để làm thay, và sáng nay trình biên dịch Rust React đã chạy tự nhiên trong Vite, trong khi Hacker News phát hiện ra IBM Bob, một tác nhân mã hóa AI. Sau đó Claude chính thức hóa Định lý cuối cùng của Fermat, và trên cùng trang nhất một đại kiện tướng Hàn Quốc đã đánh bại công cụ cờ vây mạnh nhất Trái đất, vậy là hôm nay nhân loại thắng một trong hai. Trong video này: Claude thực sự đã chứng minh gì, chi phí bao nhiêu,

0:52 tại sao nhà toán học đã dành sự nghiệp của mình cho việc này nói rằng nó không thay đổi gì và dù sao cũng rất vui mừng, và làm thế nào một con người đã đánh bại máy móc trong cờ vây. Hôm nay là thứ Sáu, ngày 4 tháng 9, và đây là The Daily Diff. Định lý cuối cùng của Fermat: không có số nguyên dương a, b, c thỏa mãn a mũ n cộng b mũ n bằng c mũ n với mọi n lớn hơn 2. Fermat đã viết nguệch ngoạc nó vào lề giấy khoảng năm 1637 và chết mà không cho xem công trình của mình, biến ông thành nhà phát triển đầu tiên đóng một yêu cầu với Works on my machine. Giải thưởng 100.000 mác vàng năm 1908 đã thu hút 621

1:25 chứng minh sai trong năm đầu tiên, và Andrew Wiles cuối cùng đã hoàn thành nó vào năm 1995, trong 129 trang mà các trọng tài mất nhiều tháng để xác minh. Chính thức hóa có nghĩa là viết lại chứng minh đó để Lean, một trợ lý chứng minh, có thể kiểm tra từng bước một cách cơ học, và Kevin Buzzard tại Imperial đã dẫn đầu một nỗ lực của con người để làm chính xác điều đó từ năm 2024; riêng bản thiết kế đã dài 86 trang. Nhà nghiên cứu của Anthropic Tianyi Peng đã hướng hàng chục tác nhân Claude vào đó thay vào đó, trên một nền tảng tên là Prove2Me giữ một DAG các câu lệnh định lý để các tác nhân biết phải chứng minh gì tiếp theo, bởi vì nếu không có nó các bầy đầu tiên

2:00 đã mất dấu ai đang chứng minh cái gì, đó là điều xảy ra khi lớp điều phối của bạn là regex với ngân sách tiếp thị. Mười một ngày sau, nút gốc đọc ĐÃ CHỨNG MINH: mười ba triệu dòng Lean, 29.500 định lý trung gian, khoảng sáu tỷ token đầu ra từ một mô hình nội bộ đại khái tương đương với Claude Fable 5.1. Bản dựng thất bại trừ khi chứng minh dựa trên chính xác ba tiên đề tiêu chuẩn của Lean: không xin lỗi, không quyết định tự nhiên, không gian lận. Kiểm tra nó cũng không rẻ: một bản dựng

2:29 từ đầu mất năm tiếng rưỡi trên 96 lõi và 153 gigabyte RAM, và tên định lý được tạo ra bằng máy, vì vậy kho lưu trữ tự mô tả là được viết để kiểm tra hơn là để đọc, điều mà tôi cũng sẽ mô tả enterprise Java như vậy. Bây giờ là mâu thuẫn. Bài đăng của Anthropic nói rằng Lean chứng minh tính đúng đắn không thể nghi ngờ. Kevin Buzzard, người đàn ông đã bị đánh bại, đã biên dịch kho lưu trữ trên một máy 500 gigabyte mà Anthropic cho ông mượn, xác nhận nó kiểm tra đúng, và sau đó viết,

2:56 trích dẫn, về mặt toán học công trình này không cho chúng ta biết điều gì. Ông đã chắc chắn 99,9 phần trăm định lý là đúng, và chứng minh không thêm toán học mới; điều nó cho thấy là những gì tự động chính thức hóa có thể làm bây giờ, và phần đó ông thực sự rất hào hứng. Ông được cấp một triệu bảng trong năm năm; Anthropic mất mười một ngày, và tính toán sơ bộ của một bình luận viên cho thấy sáu tỷ token đầu ra có giá niêm yết khoảng 300.000 đô la, vì vậy chiếc máy rẻ hơn, trừ khi bạn tính cả việc đào tạo máy, điều mà không ai làm.

3:24 Chi tiết hay nhất: email đến khi anh ấy đang ở một lễ hội âm nhạc ở Wales với một vạch sóng 4G, từ một cái tên mà anh ấy chưa từng nghe, nên anh ấy đã cho là một trò lừa bịp và đọc nó một tuần sau đó, đây là phản ứng đúng đắn với bất kỳ dòng tiêu đề nào chứa từ 'hình thức hóa đầu cuối'. Trong khi đó, con người đã gỡ lại một trận. Shin Jin-seo, kỳ thủ cờ vây số một thế giới, đã đánh bại KataGo, công cụ cờ vây mã nguồn mở mạnh nhất, hai ván một ở Seoul với lợi thế hai quân, khoảng cách giữa một chuyên gia hàng đầu và một chuyên gia tân binh.

3:50 Trận quyết định là một chiến thắng 11,5 điểm sau 221 nước cờ, giữ vững 99 phần trăm khả năng thắng từ giữa trận, và anh ấy đã mang về 250 triệu won, khoảng 170.000 đô la, cộng thêm một chiếc Genesis G90, vì vậy phần thưởng cho việc đánh bại một AI siêu phàm là 170 lần tiền thưởng của Google cho việc thoát khỏi sandbox của Chrome. Giải thích của anh ấy: ban đầu anh ấy sao chép các nước đi của AI và thua; anh ấy thắng bằng cách xây dựng bàn cờ theo phong cách riêng của mình, đó là lời khuyên hữu ích nhất về AI mà tôi đã nghe cả năm nay, và nó đến từ một trò chơi cờ bàn. Hai dòng nữa trong The Daily Diff.

4:22 Trình biên dịch Rust React từ oxc hiện đã được tích hợp sẵn trong Vite với một cờ; một cơ sở mã 1.036 tệp đã giảm từ 14,3 giây xuống còn 0,81 giây trong bước biên dịch, chủ yếu bằng cách xóa Babel khỏi package.json, cũng là quy trình chăm sóc da của tôi. Và IBM đã ra mắt Bob, một đối tác mã hóa AI chào bạn bằng "Chào, tôi là Bob", tạo ra các tác nhân phụ, hiện đại hóa mã máy tính lớn, và phát hành một sản phẩm phân tích có tên Bobalytics, vì vậy đâu đó một ngân hàng đang rất phấn khích và không ai đọc giấy phép.

4:51 Đó là rất nhiều biên độ cho một ngày thứ Sáu; nếu bạn muốn đọc điều này hơn là nghe tôi nói, The Daily Diff sẽ đến hộp thư đến của bạn mỗi sáng — miễn phí tại thedailydiff.dev, liên kết bên dưới. Vì vậy, phán quyết hôm nay: SHIP IT. Kernel nói có, Buzzard nói có, toán học không thay đổi, nhưng cách chúng ta kiểm tra toán học thì vừa mới thay đổi. Đó là The Daily Diff của hôm nay. Tôi là Niko từ Axrisi.

5:09 Hợp nhất có trách nhiệm.

Nguồn

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