Ngay trong lúc này, giới toán học lại có tin động trời.
Cao thủ lớp Yao Đại học Thanh Hoa dẫn đầu, dùng Claude hoàn toàn chinh phục được Định lý Cuối cùng của Fermat.
Đến đây, AI đã hoàn thành chứng minh toán học lớn nhất lịch sử.
Từng có thời, Định lý Cuối cùng của Fermat hành hạ con người hơn 350 năm, cần các nhà toán học dốc sức nhiều năm, viết ra 129 trang sách thiên thư mới chứng minh được.
Hôm nay, Anthropic lại tuyên bố, Claude chỉ dùng 11 ngày, đã hoàn thành chứng minh kiểm chứng máy móc đầu tiên từ đầu đến cuối cho Định lý Cuối cùng của Fermat!
Vì việc này, Claude điên cuồng gõ 13 triệu dòng mã, tạo ra 30.300 định lý có thể kiểm chứng, cuối cùng có 29.500 điều được dùng, trực tiếp đi vào chứng minh cuối cùng.
Khối lượng này, lớn gấp 5 lần còn hơn so với cơ sở dữ liệu định lý toán học lớn nhất thế giới Mathlib! Hơn nữa, toàn bộ quá trình đốt hết tới 6 tỷ Token.
Đây là chứng minh Lean lớn nhất từng được viết cho đến nay.
Tin tức vừa ra, toàn mạng chấn động. Có người kinh hô: 'Một tháng đã hình thức hóa Định lý Cuối cùng của Fermat? Cách khoe cơ bắp này, khiến giới toán học trông như ốc sên đang bò.'
Cao thủ lớp Yao Bành Thiên Dực
Vấn đề thế kỷ 350 năm, Claude 11 ngày giải quyết
Năm 1637, nhà toán học Pháp Fermat khi đang đọc sách, tùy tay viết ở lề trống trang sách một câu:
Khi số nguyên n > 2, phương trình x^n + y^n = z^n với x, y, z không có nghiệm nguyên dương.
Sau đó ông còn không quên đâm một nhát: 'Tôi tin chắc đã phát hiện một phương pháp chứng minh tuyệt diệu, tiếc là chỗ trống ở đây quá nhỏ, không viết xuể.'
Một câu nói như vậy, khiến các nhà toán học đời sau bị hành hạ sống dở chết dở hơn ba trăm năm.
Mãi đến năm 1995, nhà toán học Anh Wiles, mới dùng công cụ toán học hiện đại cao siêu, tạo ra một bài luận chứng minh 129 trang, rốt cuộc đã kết thúc vụ án treo hơn 350 năm này.
Nhưng vấn đề là: chứng minh của Wiles, thực sự quá phức tạp.
Toán học hiện đại, đã phát triển đến mức người bình thường đến đề bài còn không đọc hiểu. Chứng minh một định lý, giống như xây một chuỗi logic siêu phức tạp, chỉ cần một khâu ở giữa đứt gãy, toàn bộ sụp đổ.
Wiles lần đầu công bố năm 1993, đã bị chỉ ra một lỗ hổng chí mạng, ông lại đóng cửa đau khổ vật lộn một năm mới sửa được. Đối với loại chứng minh toán học đỉnh cao này, con người đi kiểm chứng tính đúng đắn của nó, thường cần chuyên gia đỉnh cao tiêu tốn hàng tháng thậm chí hàng năm.
Có cách nào để máy tính có thể như kiểm tra kết quả máy tính, chạy một lần là biết đúng sai không?
Có! Đây chính là 'hình thức hóa' (formalization).
Nói đơn giản, chính là dịch chứng minh toán học do con người viết, thành ngôn ngữ lập trình máy tính có thể chạy (ví dụ Lean), sau đó để máy móc từng bước suy diễn, nếu chạy thông, chứng tỏ chứng minh này tuyệt đối đúng.
Nhưng việc 'hình thức hóa' Định lý Cuối cùng của Fermat, giới toán học công nhận là công trình siêu lớn 'tính bằng năm'.
Chỉ riêng dự án do giáo sư Đại học Imperial College Kevin Buzzard khởi xướng, kế hoạch giai đoạn một đã có 86 trang!
Sau đó, Claude đến.
Việc con người dự tính làm vài năm, nó chỉ dùng 11 ngày, hơn nữa là 'cơ bản làm việc tự chủ'.
13 triệu dòng mã, 6 tỷ Token
'11 ngày, 13 triệu dòng mã' – đằng sau là kép trùng sát: mỹ học bạo lực của AI + thiết kế hệ thống tinh mật.
Hãy xem Claude cuối cùng đã làm gì:
Nó không chỉ chứng minh bản thân Định lý Cuối cùng của Fermat.
Vì chứng minh hình thức hóa phải bắt đầu từ tiên đề tầng dưới cùng, xây dựng lên từng tầng, nên Claude tiện tay chứng minh luôn hơn 29.000 định lý toán học trung gian khác cần thiết ở giữa.
Bên trong liên quan đến đại số, hình học, lý thuyết số, phân tích điều hòa...... nhiều nhánh trước đây hoàn toàn chưa được hình thức hóa, Claude trực tiếp 'khai hoang'.
Toàn bộ quá trình, con người cơ bản không can thiệp mấy.
Nhà nghiên cứu chỉ đưa một số chỉ thị cao tầng, ví dụ 'Jacobian variety với tư cách scheme ưu tiên khá cao' 'sớm thúc đẩy Mazur's torsion theorem' loại này.
Còn lại, chính là mấy chục tác nhân thông minh Claude ở đó điên cuồng đối thoại lẫn nhau, định nghĩa khái niệm, chứng minh định lý trung gian, sau đó xây lên từng tầng.
Cuối cùng, trình biên dịch Lean kiểm tra toàn bộ thông qua, chỉ phụ thuộc ba tiên đề tiêu chuẩn cơ bản nhất.
Khi chương trình chạy xong, bảng điều khiển hiện lên câu thần thánh 'PROVED' (đã chứng minh), nhật ký nội bộ của Claude cũng hào hứng:
'!!! Nút gốc Định lý Cuối cùng của Fermat đọc là PROVED...... Đây là mục tiêu của chiến dịch lần này...... Thời khắc lịch sử.'
Bạn xem, ngay cả AI tự thân cũng biết việc này có bao nhiêu.
Cao thủ hậu trường: Siêu học bá xuất thân lớp 'Yao' Đại học Thanh Hoa
Có thể chỉ huy Claude làm ra thần tích như vậy, chắc chắn không phải người thường.
Dẫn đầu, là trợ lý giáo sư Trường Kinh doanh Đại học Columbia, nhà nghiên cứu Anthropic – Bành Thiên Dực.
Lý lịch của anh chàng này, đơn giản là bản thân 'mở khóa ngoại':
Đại học 2013-2017, lớp 'Yao' Đại học Thanh Hoa, từng đoạt luận văn tốt nghiệp xuất sắc nhất, còn được vào đội tuyển quốc gia Olympic Tin học.
Tiến sĩ đến MIT, hướng nghiên cứu vận trù học (operations research), GPA tốt nghiệp đủ 5.0.
Hiện tại vừa làm trợ lý giáo sư Đại học Columbia, vừa ở Anthropic nghiên cứu công cụ tác nhân AI và hình thức hóa.
Thú vị là, nỗi ám ảnh của Bành Thiên Dực với việc 'AI tự động kiểm chứng chứng minh toán học', thực ra đến từ một 'trải nghiệm đau thương' thời đại học.
Lúc đó người hướng dẫn muốn viết thành quả trong luận văn của anh vào 'Nature', nhưng hỏi anh: 'Anh chắc trăm phần trăm chứng minh đúng chứ?'
Anh thành thật trả lời: '99% nắm chắc, nhưng dài như vậy, thực sự không thể 100% xác định.'
Chỉ vì 1% không chắc chắn đó, anh đã bỏ lỡ cơ hội lên 'Nature'.
Giờ thì tốt rồi, anh dùng AI tự tay bít cái '1%' đó.
Từ lật xe đến phong thần: Prove2Me làm sao cứu AI một mạng
Bạn tưởng rằng để AI chứng minh định lý, chính là nhập một câu 'Hãy chứng minh Định lý Cuối cùng của Fermat', nó liền phụt ra 13 triệu dòng mã?
Sai to rồi.
Lúc mới bắt đầu, thí nghiệm suýt lật xe.
Anthropic tiết lộ, giai đoạn đầu mấy chục tác nhân thông minh Claude cộng tác không lâu liền hỗn loạn hoàn toàn, như ruồi không đầu, tiến độ không theo kịp nhau, hiệu suất hợp tác thấp nổ banh. Mã từ các thử nghiệm thất bại đầu kỳ đóng góp, cuối cùng chỉ chiếm 7%.
'Chứng hay quên' và 'ảo giác' của mô hình lớn, trước mặt toán học nghiêm túc chính là vết thương chí mạng – một dòng sai, mấy triệu dòng sau toàn bộ hỏng.
Thời khắc then chốt, đội ngũ Bành Thiên Dực tạo ra nền tảng Prove2Me.
Thứ này tương đương với trang bị cho các AI một 'quản lý dự án siêu cấp', chuyên trị các loại bất phục:
Định lý DAG (cây nhiệm vụ): Cấp cho mỗi AI một bản đồ rõ ràng, nói cho nó bước tiếp theo nên chứng minh nút trung gian nào, giảm nhẹ cực lớn suy giảm trí nhớ, mấy chục tác nhân thông minh có thể hiệu suất song song.
Tách biệt phát biểu và chứng minh: Tăng tốc tốc độ biên dịch, tiết kiệm tài nguyên.
Chỉ mục ngôn ngữ tự nhiên: Mỗi định lý đều lưu mô tả bằng lời người, các AI tra cứu tái sử dụng thành quả thuận tiện hơn nhiều.
Phối hợp với khung đa tác nhân thông minh của Claude Code, các AI giống như công binh lắp định vị, trong mê cung toán học cuồng phi, 11 ngày đánh thông toàn quan.
Giới toán học phục rồi
Thành quả vừa công bố, X và các diễn đàn kỹ thuật lớn trực tiếp sóng thần.
Vị giáo sư Đại học Imperial College vốn dự định dành vài năm làm hình thức hóa đó, xem xong cũng phục, đánh giá cực cao: 'Đây là một bước tiến lớn trong tự động hình thức hóa tài liệu toán học hiện đại! Sau này có thể dùng để tra lỗi trong thư viện toán học của con người, còn có thể kiểm chứng kết luận toán học do mô hình lớn tạo ra.'
Nhưng góc nhìn của cư dân mạng càng kỳ lạ hơn.
Có người bình luận thần kỳ: 'Cách AI giải quyết toán học là – cho bạn một đáp án cực kỳ phức tạp (13 triệu dòng mã), bạn muốn chứng minh nó sai, còn khó hơn tự giải một lần. Vì vậy bạn chỉ có thể từ bỏ kháng cự, chấp nhận nó đúng rồi. Đây không phải là PUA trong giới toán học sao?'
Lại có người nói: 'Viết 13 triệu dòng mã, chỉ để khiến một định lý 350 năm ngồi ngoan ngoãn trước mặt máy móc...... Bàn của con người vẫn chưa sẵn sàng tiếp nhận thứ quy mô này.'
Tuyệt hơn nữa, Anthropic để khoe cơ bắp, còn tiện tay làm một thí nghiệm nhỏ.
Dùng 3 tài khoản bình thường, trên nền tảng Prove2Me tiêu 3 ngày, liền cũng hình thức hóa được định lý nổi tiếng 'Vinogradov's theorem' trong lý thuyết số!
Có nghĩa là, chỉ cần có công cụ thích hợp, sau này nhà khoa học dân gian mua vài tài khoản AI cấp tiêu dùng, cũng có thể đi kiểm chứng định lý toán học đỉnh cao nhất của con người rồi!
AI sẽ không thay thế nhà toán học, nhưng sẽ thay đổi hoàn toàn toán học
Vậy, nhà toán học có phải thất nghiệp không?
Anthropic chính thức cho đáp án: Sẽ không thay thế, nhưng sẽ thay đổi hoàn toàn cách chơi.
Trong lịch sử, kiểm chứng toán học có nhiều 'bi kịch'.
Ví dụ năm 1998 có người chứng minh giả thuyết Kepler, hội đồng thẩm định tiêu tốn 4 năm, cuối cùng chỉ có thể nói '99% chắc chắn'; Perelman chứng minh giả thuyết Poincaré, toàn bộ giới toán học tiêu tốn 4 năm viết 3 cuốn sách hơn 300 trang mới miễn cưỡng hiểu được; còn có định lý, bị coi là chân lý chấp nhận mấy năm, người khác xây lầu trên đó, cuối cùng phát hiện móng là sụp.
Mà công nghệ Claude mang đến, chính là muốn kết thúc loại 'tính không chắc chắn' này.
Tương lai, AI không chỉ là máy tính của nhà toán học, càng là trọng tài nghiêm khắc nhất.
Khi AI có thể nhanh chóng tạo ra hàng ngàn hàng vạn phỏng đoán và chứng minh mới, con người xem không xuể, vậy thì biến 'đính kèm mã kiểm chứng hình thức hóa' thành tiêu chuẩn của luận văn.
Thời đại mô hình lớn, hình thức hóa tự động quy mô lớn dùng cách tiếp cận kỹ thuật hóa, mở ra khả năng mới.
Tài liệu tham khảo:
https://www.anthropic.com/research/formalizing-fermats-last-theorem
Biên tập: Aeneas
Bài viết này từ tài khoản công chúng WeChat "Tân Trí Nguyên" (ID:AI_era), tác giả: ASI Khải Thị Lục
