09 Sep 2026 · 8 phút đọc
ai
Claude hình thức hóa Định lý cuối của Fermat bằng Lean: 13 triệu dòng chứng minh máy-kiểm-tra dạy gì cho người xây agent
Claude của Anthropic tạo ra một chứng minh Lean dài 13 triệu dòng, được máy xác minh toàn bộ, cho Định lý cuối của Fermat trong 11 ngày thông qua bộ điều phối mã nguồn mở Prove2Me. Góc nhìn Tech Lead: pattern điều phối đa agent phía sau nó có ý nghĩa gì cho bất kỳ team nào đang xây agent tự động chạy dài hạn.
Đọc tiếp







