- Phần chưa được giải của bài toán phân rã Hamilton do Donald Knuth nêu ra đã được mở rộng lời giải nhờ sự hợp tác giữa con người và AI
- Claude đã tìm ra lời giải cho m lẻ và được đặt tên là “Claude’s Cycles”; sau đó 996 trong số 11.502 chu trình đã được tổng quát hóa cho mọi m lẻ
- Dr. Ho Boon Suan dùng GPT-5.4 Pro để thực hiện bản chứng minh dài 14 trang cho m chẵn ≥ 8 và kiểm chứng tính toán đến m=2000
- Dr. Keston Aquino-Michaels đã tìm ra một phương pháp cấu thành đơn giản cho cả m lẻ và m chẵn bằng quy trình đa tác tử với GPT và Claude
- Dr. Kim Morrison đã kiểm chứng hình thức lời giải của Knuth bằng trợ lý chứng minh Lean, hoàn thiện hệ sinh thái hợp tác giữa con người, AI và công cụ chứng minh
Mở rộng hợp tác để giải bài toán Claude’s Cycles
- Phần chưa được giải của bài toán phân rã Hamilton do Donald Knuth nêu ra đã được giải nhờ sự hợp tác giữa con người và AI
- Ban đầu, Claude đã tìm ra lời giải cho m lẻ sau khoảng một giờ tìm kiếm, và Knuth đặt tên cho nó là “Claude’s Cycles”
- Trong bài báo được cập nhật sau đó, với trường hợp cơ sở m=3, tồn tại chính xác 11.502 chu trình Hamilton, trong đó 996 chu trình được tổng quát hóa cho mọi m lẻ
- Knuth xác nhận 760 phép phân rã “kiểu Claude” hợp lệ trong số này
- Với m chẵn, Claude chưa hoàn tất được, nhưng Dr. Ho Boon Suan đã sử dụng GPT-5.4 Pro để viết bản chứng minh dài 14 trang cho m≥8 và thực hiện kiểm chứng tính toán đến m=2000
- Tiếp đó, Dr. Keston Aquino-Michaels đã phát hiện một phương pháp cấu thành đơn giản có thể áp dụng cho cả m lẻ lẫn m chẵn thông qua quy trình đa tác tử sử dụng đồng thời GPT và Claude
- Dr. Kim Morrison đã hình thức hóa và kiểm chứng lời giải cho trường hợp m lẻ của Knuth trong trợ lý chứng minh Lean
- Kết quả là một hệ sinh thái hợp tác toán học hoàn chỉnh đã được hình thành, nơi con người, nhiều hệ thống AI và công cụ chứng minh hình thức cùng phối hợp song song
- Chuỗi tiến triển này khởi đầu từ việc một AI giải một bài toán đơn lẻ, rồi mở rộng thành mô hình nghiên cứu toán học mới với sự hợp tác giữa nhiều AI, con người và trợ lý chứng minh
- Bài báo mới nhất được công bố trên website Stanford CS Faculty(www-cs-faculty.stanford.edu/~knuth/papers/)
1 bình luận
Ý kiến trên Hacker News
Tôi luôn nói rằng AI sẽ giành Huy chương Fields trước khi vận hành McDonald's
Toán học đối với con người khó như dùng búa để vặn ốc vít
LLM mạnh ở việc khám phá nông nhưng rộng, nên đang tìm ra nhiều mẫu toán học mới
Tôi dự đoán sau này sẽ chuyển từ LLM sang học tăng cường kiểu AlphaGo dựa trên cây cú pháp Lean
Nếu có thể mã hóa ‘10 mẹo’ mà các nhà toán học dùng thành vector tiềm ẩn thì coi như game over
Chúng ta tư duy bằng cách áp dụng hình học đại số vào các bài toán số học thông qua suy luận tương tự hình học
AI được huấn luyện trên cây Lean có thể còn sở hữu một hệ trực giác rộng hơn con người
Giống như trường hợp StockFish trong cờ vua, cách tiếp cận này đáng để nghiên cứu dưới góc nhìn mechanistic interpretability
Việc lấy mẹo ra dùng thì LLM giờ cũng đã làm khá tốt
Nhưng phần biểu diễn bài toán cho đúng vẫn là việc của con người, và điều đó là tự nhiên
Tôi muốn thêm vào phiên bản của mình: nghề được tự động hóa sau cùng sẽ là QA
Làn sóng công nghệ này khiến chúng ta phải suy nghĩ lại về bản chất của lao động tri thức, và nhờ đó chúng ta sẽ sắc bén hơn
Từ sau khi biết câu châm ngôn 4chan “trolls trolling trolls”, tôi luôn nhìn các tương tác trên Internet bằng con mắt hoài nghi
Tôi từng cảm thấy Reddit đã là một ‘internet chết’, nhưng nhìn thread này thì giờ không còn phân biệt được đâu là bot đâu là người
Vì vậy tôi đã tạo ra dịch vụ RememberBuddy — một nơi lưu lại những insight đời thường để không quên chúng
Sự tiến hóa của AI trong toán học có lẽ sẽ đi theo quỹ đạo mà Greg Egan đã dự báo trong tiểu thuyết từ thập niên 90
Bản chất của toán học không đổi, nhưng lý do chúng ta làm toán sẽ thay đổi
Trong Diaspora của Egan, khám phá toán học được mô tả như đào ngọc trong mỏ muối
Có người theo đuổi vẻ đẹp thuần khiết của chính viên ngọc đó, người khác lại tìm giá trị thực dụng
Những nơi như viện nghiên cứu mà Terence Tao lập ra hiện nay phần nào đã chạm tới tương lai đó
Trong ngắn hạn, kiểu nghiên cứu này sẽ cải thiện rất nhiều khả năng tạo ra thông tin chính xác của các hệ thống AI
Một số người cho rằng khám phá tri thức chỉ đơn thuần là bắt chước hành vi trong quá khứ, nhưng tôi không nghĩ vậy
Nếu chuyên gia dẫn dắt mô hình tốt thì phần lớn vấn đề đều có thể giải quyết
Mô hình là công cụ tuyệt vời để làm thay phần việc lười làm của chuyên gia, nhưng với các vấn đề phức tạp thì vẫn còn điểm mù
Tôi đã thấy một phần system prompt trong bài báo,
có quy tắc rằng: “hãy cập nhật
plan.mdngay sau mỗi lần chạy exploreXX.py”Tôi tò mò vì sao những prompt như vậy lại cải thiện hiệu năng giải quyết vấn đề nâng cao
Chúng ta đang ngày càng tiến gần hơn tới viễn cảnh “intelligence as a subscription” mà CEO OpenAI từng nói đến
Việc giảm chuyển tab đang bị đánh giá thấp
Một nửa số công cụ AI không phải đang giải quyết bài toán UX mà là cuộc chiến đảm bảo độ ổn định của việc truy cập mô hình
“Nếu đưa cho 100 con khỉ 100 khẩu súng và vật liệu xây dựng, chúng sẽ xây nhà hay cướp ngân hàng?”
Nếu ra kết quả nào đó, tôi muốn hỏi liệu đó có phải là hành vi có chủ đích hay không
Tôi đã xem tweet này