Claude giúp giải mã 16 sổ tay Gödel, liệt kê 663 định lý, Coq kiểm chứng, vậy công thuộc về ai

16 sổ tay Gödel viết từ đầu thập niên 1940, Claude trả về bản giải thích 650 trang trong vài ngày cùng danh mục 663 định lý, và Jan von Plato nói ông choáng váng. Điểm cần biết là Claude không tự đọc chữ viết tay tốc ký, von Plato đã phiên âm suốt 9 năm, và mọi con số lớn chỉ có một nguồn gốc là lời von Plato kể với Guardian ngày 13/11/2026.

Tóm tắt nhanh: 16 sổ tay Gödel, 1.009 trang theo lời von Plato qua Guardian 13/11/2026, Claude trả về bản giải thích 650 trang và 663 định lý, Coq kiểm chứng khoảng 400 đúng, khoảng 200 cần sửa, khoảng 50 sai. Các con số đều là ước lượng, theo lời von Plato qua một nguồn duy nhất là Guardian, chưa qua bình duyệt độc lập.

Chuỗi 4 mắt xích von Plato làm 9 năm rồi Claude mới vào cuộc

Mình kể chuỗi này trước, vì kể sai là hỏng cả bài, nhiều bản tin viết gọn thành Claude tự làm hết.

9 năm phiên âm tốc ký Gabelsberger của Jan von Plato ở Helsinki

Jan von Plato bắt đầu dự án Gödel năm 2017 ở Helsinki, với tài trợ 2,5 triệu euro từ European Research Council. Ông tự học tốc ký Gabelsberger rồi phiên âm, khoảng một trang mỗi tuần, tức một năm nhóm ông đọc khoảng 50 trang, tới tháng 9/2026 đã có bản ghi chép toàn bộ 16 workbook cùng 6 cuốn sách. Tổng số trang có ba cách đếm: Guardian nói 1.009, Helsinki nói khoảng 1.200, AITP nói khoảng 1.700.

Claude nhận bản phiên âm và trả về bản giải thích 650 trang trong vài ngày

Tháng 9/2026, von Plato đưa cho Claude bản ghi chép, 6 cuốn sách và tài liệu khoa học thứ cấp. Trong vài ngày, Claude trả về bản giải thích 650 trang cùng danh mục 663 định lý, và von Plato nói ông choáng váng. Claude nối được mọi mảnh trong 1.000 trang thành một khối, điều con người làm chậm vì hay quên.

Von Plato kiểm tra từng trang và tự chạy Coq chứ Claude không tự chứng minh

Von Plato nhấn mạnh bản 650 trang phải kiểm tra từng trang, và chính ông là người chạy các chứng minh tái dựng qua Coq, vì Claude không tự đọc tốc ký, không tự chứng minh, không chạy Coq, mà giải mã tốc ký khó hơn đọc chữ viết tay nhiều bậc. Mốc gợi ý dùng AI chưa khớp: Guardian viết tháng 8/2026, slide AITP ghi ngày 3/9/2026.

Con số 663 định lý gộp 3 mức độ và Coq chia thành khoảng 400, khoảng 200, khoảng 50

Anh em để ý con số 663, vì đây là con số dễ bị đọc sai nhất trong cả vụ việc.

663 định lý gộp ba mức độ khác nhau chứ không phải 663 định lý đã chứng minh

663 là số định lý Claude liệt kê khi von Plato yêu cầu trích xuất mọi định lý mà Gödel đã có chứng minh, phác thảo hoặc ý tưởng, tức là một chứng minh đầy đủ, một phác thảo hay một ý tưởng đều được đếm chung vào 663, nên 663 không có nghĩa là 663 định lý đã chứng minh.

Coq trả về khoảng 400 định lý đúng như Gödel phát biểu

Khoảng 400 định lý qua được Coq đúng như phát biểu, chiếm khoảng 60% tổng số, và mình nhắc lại, các con số đều là số ước lượng do von Plato nói. Ba nhóm cộng lại khoảng 650, gần bằng 663, vì các con số đều là ước lượng. Kiểu kiểm chứng bằng máy này không còn xa lạ, như vụ AI chứng minh giả thuyết Aaronson-Ambainis mà Aaronson xác nhận tin được.

Khoảng 200 định lý cần sửa và khoảng 50 định lý sai thì công thuộc về ai

Khoảng 200 định lý cần sửa, nghĩa là phát biểu phải chính xác hơn hoặc thêm giả thiết mới qua được, chiếm khoảng 30%, còn khoảng 50 sai hẳn, chiếm khoảng 8%. Gödel khi đọc lại đôi khi tự ghi bên lề falsch hoặc schlecht, nghĩa là sai hoặc tệ, nên định lý sai trong sổ tay nháp là bình thường. Việc sửa 200 định lý đặt ra câu hỏi về quyền công trạng, vì phát biểu đúng cuối cùng là của ai.

Chứng minh tiên đề chọn năm 1966 và chuyện Gödel chỉ còn một bước nữa

Mình thấy đây là phát hiện được chú ý nhất trong cả vụ việc.

Gödel chứng minh nửa nhất quán năm 1938 rồi Cohen giành Fields 1966 bằng forcing

Năm 1938, Gödel chứng minh giả thuyết continuum và tiên đề chọn nhất quán với ZF bằng vũ trụ constructible. Đầu năm 1963, Paul Cohen tìm ra phương pháp forcing, chứng minh nửa còn lại, tức là giả thuyết continuum không thể chứng minh được từ ZFC, rồi giành Huy chương Fields 1966, huy chương đầu tiên trao cho logic toán học. Cohen hỏi trực tiếp, Gödel đáp đã chứng minh bằng phương pháp liên quan tới phương pháp của Cohen, nhưng không đưa ra ý tưởng chính xác nào.

Claude tái dựng chứng minh tiên đề chọn, Gödel chỉ còn một bước nữa vì một định nghĩa viết sai

Von Plato giao cho Claude nhiệm vụ đầu tiên là tìm chứng minh tính độc lập của tiên đề chọn trong workbook, và câu trả lời là có, gần như vậy, Gödel chỉ còn một bước nữa. Một định nghĩa Gödel viết sai nhưng ông đã dùng đúng hai năm trước đó, nên von Plato cho rằng Gödel chỉ cần thêm vài tháng. Von Plato chạy bản tái dựng qua Coq thì nó đạt. Helsinki xác nhận nhóm đã biết chứng minh năm 1942 từ trước khi dùng Claude. Chuyện AI làm việc với giả thuyết toán học lớn cũng đang xuất hiện, như vụ OpenAI và Anthropic cùng bác bỏ giả thuyết ETH bằng thuật toán đếm 3-SAT.

Dữ kiện, suy luận của von Plato và ý kiến của Hamkins về chứng minh tiên đề chọn

Lớp thứ nhất là dữ kiện, sổ tay chứa các mảnh chứng minh và bản tái dựng qua được Coq, lớp thứ hai là suy luận của von Plato, Gödel lẽ ra đã tới đích nếu tiếp tục vài tháng, có thể đã giành Fields 1940, và von Plato cho rằng Gödel có thể đã cảm thấy tiếc khi Cohen nhận Fields 1966, còn lớp thứ ba là ý kiến của Hamkins, giống chứng minh của Cohen không có nghĩa là Gödel đã có nó, và không ai được công nhận cho việc mình không công bố.

Hamkins và Hacker News nói gì khi nghe tin Claude giải mã sổ tay Gödel

Guardian đã đưa đối trọng Hamkins ngay trong bài gốc, và mình thấy chỗ này đáng đọc kỹ.

Hamkins công nhận bản tái dựng chứng minh tiên đề chọn nhưng giao quyền công trạng cho sử gia

Joel David Hamkins, giáo sư logic Đại học Notre Dame, nói với Guardian rằng nếu bản tái dựng đứng vững thì nó đáng chú ý về lịch sử, nhưng bao nhiêu là của Claude và bao nhiêu là của Gödel là việc của các sử gia. Hamkins nói rõ ông chưa xem bản tái dựng. Chưa có chuyên gia thứ hai nào ngoài Hamkins lên tiếng.

Hacker News nghi ngờ con số sáu người đọc được tốc ký Gabelsberger

Mình thấy Hacker News nghi ngờ con số sáu người mà von Plato tự nhận. hobo123 kể cha anh ta viết ghi chú bằng Gabelsberger tự chế tới khi mất năm 2020, còn semolinapudding đọc hẹp lại là 6 người vừa đọc được vừa hiểu logic toán. rsoto2 chê thị giác máy tính đã làm được việc này từ lâu, nhưng Perseids phản bác bằng slide cho thấy tốc ký không nhận ra được. 2aFds nghi thời điểm tin ra gần một đợt IPO, và cho rằng mô hình được huấn luyện trên bản ghi chép có sẵn, nhưng cả hai đều là suy đoán, chưa có bằng chứng.

Tranh luận Newton và Leibniz và chuyện Gödel chỉ công bố thứ không thể bắt bẻ

iltennico cảnh báo Gödel chỉ công bố công trình không thể bắt bẻ, còn bananaflag phản bác bằng Dialectica interpretation, nghĩ ra năm 1940 nhưng tới 1958 mới công bố. sheikhnbake lo giá trị của von Plato sẽ mờ dần khi AI dịch xong, còn alterom nói đây là ví dụ dùng AI để không bị lỗi thời, rồi so sánh với Newton và Leibniz.

Coq kiểm tra cái gì và không kiểm tra cái gì

Anh em nào chưa quen với Coq thì mình nói gọn, Coq là gì, và vì sao qua được Coq lại quan trọng?

Coq nay gọi là Rocq, ra đời năm 1989 và từng kiểm chứng định lý bốn màu

Coq, nay là Rocq, là chương trình kiểm tra tính đúng đắn hình thức của chứng minh toán học, phát hành lần đầu năm 1989, đổi tên với bản Rocq 9.0 tháng 3/2025. Coq từng kiểm chứng định lý bốn màu năm 2005 và Feit-Thompson năm 2012, nhận giải ACM Software System Award 2013.

Coq kiểm tra từng bước suy luận có đúng logic hay không

Coq kiểm tra một chứng minh viết bằng ngôn ngữ hình thức, từng bước có đúng logic hay không, và nó không tự nghĩ ra chứng minh. Von Plato là người chạy Coq, và đưa định lý vào Coq đòi hỏi diễn đạt lại bằng ngôn ngữ hình thức. DeepMind cũng kiểm chứng kiểu này, như vụ DeepMind dùng AlphaProof và Code chứng minh toán học mã hóa Signal trong 4 tuần.

Coq không đánh giá ý nghĩa, tính gốc hay phát biểu gốc có phải của Gödel

Mình thấy giới hạn này quan trọng không kém: Coq không đánh giá ý nghĩa hay tính gốc của một định lý, không kiểm tra phát biểu gốc có phải của Gödel. Coq xác nhận chỉ có nghĩa là chứng minh đã qua kiểm tra hình thức, không có nghĩa là cộng đồng đã công nhận đó là mới. Việc 200 định lý phải sửa mới qua được Coq cho thấy bước diễn đạt lại cũng góp phần tạo ra định lý đúng.

Claude tái dựng chứ không khám phá mới, và những thứ chưa ai kiểm chứng được

Mình tạm gác chuyện ai có công sang một bên, trước hết cần hỏi lại, nên hiểu cụm AI khám phá thế nào cho đúng?

Tái dựng khác khám phá mới, và Feedzop thổi phồng chuyện sổ tay Gödel ra sao

Claude không phát hiện ra toán học từ con số không, mà giúp một chuyên gia đọc hiểu kho tài liệu đã phiên âm 9 năm nhanh hơn. Khám phá ở đây là những kết quả Gödel đã viết từ thập niên 1940 nhưng không ai đọc được suốt hơn 80 năm, nay mới được hệ thống hóa. Feedzop viết Gödel đi trước thời đại vài thế kỷ, Guardian chỉ nói đi trước thời đại rất xa.

Danh sách những thứ chưa ai biết gồm phiên bản Claude và danh sách 663 định lý

Anh em để ý danh sách này: chưa biết phiên bản Claude nào được dùng, chưa thấy bản 650 trang và danh sách 663 định lý công khai ở đâu, chưa biết 14 chủ đề logic là những chủ đề nào, và chưa rõ hơn một chục chủ đề cuối bài có phải cùng 14 chủ đề đó hay không. Chưa biết khi nào có công bố khoa học, chưa có thông báo chính thức của Anthropic tính tới 14/11/2026, chưa có thread Reddit thảo luận sâu. Hamkins nói rõ ông chưa xem bản tái dựng, và tuổi 75 của von Plato chưa có nguồn đối chiếu.

Bước tiếp theo là sổ tay vật lý và vũ trụ học của Gödel

Von Plato nói sổ tay vật lý và vũ trụ học của Gödel là vùng đất chưa biết, ông sẽ khám phá sau khi xong các dự án logic. Cộng đồng đang chờ bản công bố khoa học, và von Plato đã trình bày về giải mã Gödel tại AITP 2026 và Vienna Circle 19/10/2026.

Kết lại, nên tin vụ giải mã sổ tay Gödel tới mức nào

Mình gom lại thành một câu trả lời gọn.

Mình gom lại thế này, anh em cứ tin phần đã chắc, là sổ tay chứa các mảnh chứng minh và bản tái dựng qua được Coq, rồi chờ phần cần kiểm chứng, là danh sách 663 định lý và bản 650 trang, còn chuyện Gödel lẽ ra đã giành Fields 1940 và câu hỏi ai có công thì cứ để ở vị trí suy luận và ý kiến. Hướng khám phá tiếp theo đã rõ, sổ tay vật lý và vũ trụ học của Gödel, còn câu hỏi Newton và Leibniz thì vẫn còn đó.

Nguồn tham khảo

The Guardian, bài gốc 13/11/2026, URL gốc chưa mở trực tiếp được, đã đọc qua bản đăng lại: https://www.theguardian.com/science/2026/nov/13/kurt-godel-notebooks-ai-helps-unlock-hidden-discoveries
indianews16, bản đăng lại toàn văn: https://www.indianews16.com/ahead-of-his-time-ai-helps-unlock-discoveries-hidden-notebooks-of-man-who-transformed-maths
Mezha: https://mezha.net/eng/news/mezha-5bfca8e96e5185cfd3400769_claude_helps_uncover/
UA.News: https://ua.news/en/world/shi-dopomig-viiaviti-v-notatkakh-gedelia-sotni-nevidomikh-teorem-the-guardian
AI Weekly: https://aiweekly.co/alerts/von-plato-uses-claude-to-extract-663-theorems-from-gdel-notes
IAS, bản đăng lại: https://www.ias.edu/news/ahead-his-time-ai-helps-unlock-discoveries-hidden-notebooks-man-who-transformed-maths
Santa Ana Herald: https://www.santaanaherald.com/stories/ahead-of-his-time-ai-helps-unlock-discoveries-hidden-notebooks-of-man-who-transformed,2249351
Hacker News, thread: https://news.ycombinator.com/item?id=50486748
Helsinki, dự án Gödel Enigma: https://www.helsinki.fi/en/researchgroups/godel-enigma/research/project-description
AITP, slide Deciphering Gödel: https://aitp-conference.org/2026/slides/JvP.pdf
Springer, Results on Foundations: https://link.springer.com/book/10.1007/978-3-031-37875-1
Wikipedia, Rocq (Coq): https://en.wikipedia.org/wiki/Coq_(software)