Claude giải mã sổ tay tốc ký của Gödel, tìm ra 663 định lý
Bắt đầu từ đây
Nhà logic học người Phần Lan Jan von Plato đã dùng Claude của Anthropic để xử lý 1.009 trang sổ làm việc viết bằng tốc ký Gabelsberger của Kurt Gödel từ thập niên 1940, một công việc trước đó chỉ tiến triển khoảng một trang mỗi tuần. Trong vài ngày, Claude đã tạo ra bản giải thích dài 650 trang và xác định 663 định lý mà Gödel đã chứng minh, phác thảo hoặc hình dung. Von Plato cho biết kết quả đầu ra phải được kiểm tra từng trang một. Khi chạy qua trợ lý chứng minh Coq, khoảng 400 định lý được xác minh đúng như đã nêu, khoảng 200 cần sửa — ví dụ cần phát biểu chính xác hơn hoặc thêm giả thiết — và khoảng 50 định lý là sai. Von Plato cho biết việc Claude tái dựng một chứng minh về tính độc lập của tiên đề chọn lọc, vốn đã vượt qua Coq, gợi ý rằng Gödel đã có kết quả này từ thập niên 1940, và các sổ làm việc còn chứa hơn một chục chủ đề logic chưa được khai thác.
Tạo từ các bài viết · cập nhật 1 giờ trước
Dòng thời gian bài viết
Theo các bài viết để thấy sự việc từ nhiều phía.
- Hacker News · AITuyển chọnAI mở khóa sổ tay của Gödel, hé lộ hàng trăm định lý đã được chứng minh
Nhà logic học người Phần Lan Jan von Plato đã dùng Claude để xử lý 1.009 trang sổ làm việc viết bằng tốc ký Gabelsberger của Kurt Gödel từ thập niên 1940, một công việc trước đó chỉ tiến triển khoảng một trang mỗi tuần. Claude đã tạo ra một bản giải thích dài 650 trang và xác định 663 định lý mà Gödel đã chứng minh, phác thảo hoặc hình thành ý tưởng; khi chạy qua trợ lý chứng minh Coq, khoảng 400 định lý được xác nhận đúng như đã nêu, khoảng 200 cần sửa chữa và khoảng 50 là sai. Von Plato cho biết việc Claude tái dựng một chứng minh về tính độc lập của tiên đề chọn lọc, đã vượt qua Coq, gợi ý rằng Gödel đã có kết quả này từ thập niên 1940, và rằng các sổ làm việc chứa hơn một chục chủ đề logic chưa được khám phá.
Độ nóng của sự việc này
Chưa đủ quan sát liên tục để vẽ xu hướng.