Anthropic hoàn thành chứng minh hình thức hóa Định lý lớn Fermat bằng Lean

T7 · 05/09

1. 06:30

   Anthropic thông báo Claude đã hoàn thành chứng minh hình thức đầu tiên từ đầu đến cuối cho Định lý lớn Fermat trong 11 ngày

   IT Home

   Vào ngày 4 tháng 9, Anthropic công bố rằng sau 11 ngày vận hành gần như tự chủ, Claude đã hoàn thành chứng minh hình thức bằng Lean đầu tiên từ đầu đến cuối cho Định lý lớn Fermat, đồng thời đã được máy tính kiểm chứng.

   Đọc bản tiếng Việt →Đọc bài gốc ↗
2. 06:10

   Claude hoàn thành chứng minh hình thức hóa đầu tiên bằng máy tính cho Định lý lớn Fermat

   X: Kim (@kimmonismus)

   Anthropic thông báo Claude đã hoàn thành chứng minh hình thức hóa đầu tiên cho Định lý lớn Fermat. Quá trình này mất 11 ngày với tổng cộng hơn 13 triệu dòng mã Lean, trở thành chứng minh Lean lớn nhất từ trước đến nay.

   Đọc bản tiếng Việt →Đọc bài gốc ↗
3. 03:10

   Claude hoàn thành bản chứng minh hình thức hóa Định lý lớn Fermat trên Lean trong 11 ngày

   X: Rohan Paul (@rohanpaul_ai)

   Anthropic thông báo Claude đã hoàn thành bản chứng minh Định lý lớn Fermat đầu tiên được kiểm chứng hoàn toàn bằng máy. Trong vòng 11 ngày, Claude đã sử dụng nhiều tác nhân (agent) để chuyển đổi bản chứng minh dựa trên Wiles thành mã Lean.

   Đọc bản tiếng Việt →Đọc bài gốc ↗
4. 03:02

   Anthropic sử dụng Claude để hoàn thành bản chứng minh hình thức hóa Định lý lớn Fermat trên Lean trong 11 ngày

   Hacker News Nổi bật (buzzing.cc bản dịch tiếng Trung)

   Anthropic thông báo đạt được bản chứng minh Định lý lớn Fermat đầu tiên được máy tính xác thực hoàn toàn. Trong 11 ngày, Claude đã tự viết gần như toàn bộ 13 triệu dòng mã Lean, chứng minh và sử dụng 29.500 định lý trung gian, với quy mô gấp hơn 5 lần Mathlib.

   Đọc bài gốc ↗
5. 02:59

   Anthropic đăng tải bản chứng minh Định lý lớn Fermat được kiểm chứng bằng máy dựa trên Lean 4; Ethan Mollick chỉ ra rằng tài liệu vẫn mang phong cách của Claude

   X: Ethan Mollick (@emollick)

   Anthropic đã đăng tải bản chứng minh Định lý lớn Fermat được kiểm chứng bằng máy hoàn chỉnh trên Lean 4 lên GitHub (https://github.com/anthropics/fermats-last-theorem), dựa trên Mathlib (Lean 4.33.1, Mathlib v4.33.0) với lộ trình lập luận qua Frey, Serre, Ribet, Wiles và Taylor-Wiles. Ethan Mollick đã chia sẻ và bình luận rằng, dù mô tả về bản chứng minh này khá ngắn gọn, nhưng cách viết "đặt tên cho từng bước và chú thích định lý Lean tương ứng" trong tệp PROOF-PATH.md vẫn rất giống sản phẩm của Claude. Kho lưu trữ này được đánh dấu là sản phẩm nghiên cứu, không duy trì và không nhận đóng góp.

   Đọc bản tiếng Việt →Đọc bài gốc ↗
6. 01:58

   Claude hoàn thành chứng minh hình thức hóa Định lý lớn Fermat, tạo ra hơn 13 triệu dòng mã Lean

   X: Anthropic (@AnthropicAI)Chính chủ

   Anthropic thông báo Claude đã hoàn thành chứng minh hình thức hóa đầu tiên cho Định lý lớn Fermat vào tháng trước, đây là chứng minh bằng Lean lớn nhất từ trước đến nay.

   Đọc bản tiếng Việt →Đọc bài gốc ↗
7. 01:37

   Anthropic sử dụng Claude để hoàn thành chứng minh hình thức hóa bằng Lean đầu tiên được máy tính xác thực cho Định lý lớn Fermat trong vòng 11 ngày

   Anthropic: Research (công bố - Web)Chính chủ

   Anthropic công bố chứng minh Định lý lớn Fermat đầu tiên được máy tính xác thực hoàn chỉnh. Claude đã thực hiện phần lớn quá trình hình thức hóa một cách tự chủ trong 11 ngày, viết ra 13 triệu dòng mã Lean và chứng minh 30.300 định lý (cuối cùng sử dụng 29.500 định lý trong số đó), với quy mô gấp hơn 5 lần Mathlib.

   Đọc bản tiếng Việt →Đọc bài gốc ↗