Tuần này Anthropic công bố nghiên cứu cho thấy Claude đã tạo ra chứng minh đầy đủ, từ đầu đến cuối, được máy tính kiểm tra hoàn toàn cho Định lý cuối của Fermat bằng ngôn ngữ chứng minh định lý Lean — 13 triệu dòng chứng minh hình thức, hơn 5 lần kích thước của Mathlib (toàn bộ thư viện toán học hình thức hóa hiện có của cộng đồng), hoàn thành trong 11 ngày phần lớn một cách tự động. Tôi muốn bỏ qua tiêu đề kiểu “AI làm toán cao cấp”, vì con số thực sự quan trọng với tôi với tư cách Tech Lead nằm sâu hơn bên dưới: lần thử đầu tiên thất bại, và nó chỉ thành công sau khi một công cụ điều phối mã nguồn mở của một team khác, Prove2Me, được gắn thêm vào giữa chừng.
Đây không phải câu chuyện về năng lực model. Đây là câu chuyện về điều phối agent chạy dài hạn, và là case study công khai cụ thể nhất mà tôi từng thấy về việc điều gì thực sự đổ vỡ khi bạn mở rộng một workload agent vượt quá những gì một context window đơn hay một phiên agent đơn có thể chứa.
Vì sao Định lý cuối của Fermat là một benchmark agent khắc nghiệt
Hình thức hóa một chứng minh cỡ này bằng Lean nghĩa là mỗi dòng trong 13 triệu dòng đó phải type-check được với một proof assistant không khoan nhượng cho bất kỳ sự mơ hồ nào — không có điểm cộng một phần, không có “gần đúng là được”, không có khoảng trống suy luận phi hình thức kiểu một nhà toán học có thể để một bước là “rõ ràng đúng”. Chứng minh của Claude thiết lập hơn 29.000 định lý bổ trợ trong quá trình đó, trải khắp các lĩnh vực toán học chưa từng được hình thức hóa trước đây. Điều này có nghĩa công việc không thể được thực hiện bởi một agent duy nhất giữ toàn bộ vấn đề trong context. Nó phải được phân rã, phân phối, theo dõi, và ráp lại chính xác qua một đội agent, theo mô tả của Anthropic, chạy trong khoảng hai tuần, tiêu tốn khoảng sáu tỷ output token.
Đó là phần đáng để nghiên cứu bất kể bạn có quan tâm đến lý thuyết số hay không.
Prove2Me thực sự giải quyết điều gì
Prove2Me, được xây dựng từ Đại học Columbia và mã nguồn mở, duy trì một đồ thị có hướng không chu trình (DAG) của các phát biểu định lý và điều phối nhiều agent Claude làm việc trên đó. Hai quyết định thiết kế nổi bật dưới góc nhìn kỹ thuật:
- Tách phát biểu (statement) khỏi chứng minh (proof) thành các file riêng, liên kết độc lập với nhau. Biên dịch Lean chậm, và việc xác minh lại toàn bộ một file chứng minh khổng lồ monolithic mỗi khi có thay đổi thì không mở rộng được. Bằng cách tách phát biểu của một định lý khỏi chứng minh của nó, Prove2Me cho phép các agent khác xây dựng dựa trên phát biểu định lý ngay cả khi chứng minh của nó chưa hoàn thành — tương tự như việc code dựa trên một interface trước khi phần implementation ra đời.
- Một mô tả bằng ngôn ngữ tự nhiên gắn với mỗi node định lý, cho phép tìm kiếm và tái sử dụng. Các agent làm việc trên một chứng minh con có thể phát hiện ra rằng một bổ đề liên quan đã tồn tại ở nơi khác trong DAG thay vì phải suy ra lại từ đầu — tương đương trong toán hình thức của việc “đừng viết lại một hàm tiện ích, hãy tìm trong codebase trước.”
Nếu bạn thay “định lý” bằng “microservice” và “trình type-checker Lean” bằng “pipeline CI”, đây chính là một pattern đồ thị phụ thuộc (dependency graph) và phát triển interface-trước mà lẽ ra phải trông rất quen thuộc. Cái mới không phải là pattern — mà là việc một team nghiên cứu phải tái phát minh nó từ đầu, giữa chừng dự án, vì chế độ mặc định (các agent đổ các lần thử chứng minh vào một context chung) đã đâm vào tường.
Failure mode đáng để bạn lo lắng
Chi tiết mà Anthropic báo cáo thẳng thắn: lần thử hình thức hóa đầu tiên đã thất bại. Không phải “tạo ra một chứng minh hơi sai” — mà thất bại hoàn toàn, trong một lĩnh vực mà chứng minh hình thức “gần đúng” là vô giá trị vì Lean từ chối bất cứ thứ gì không type-check trọn vẹn. Đó là một điểm dữ liệu hữu ích chống lại luận điểm hiện tại rằng việc mở rộng các đàn agent (agent swarm) chủ yếu chỉ cần thêm compute và context window lớn hơn. Nó cần hạ tầng điều phối tốt hơn — phân rã tác vụ, theo dõi phụ thuộc, và tái sử dụng — được xếp chồng lên trên năng lực model frontier, chứ không phải thay thế cho nó.
Tôi sẽ ánh xạ điều này trực tiếp vào các nền tảng agent nội bộ mà tôi từng thấy (và từng xây): lần đầu tiên bạn thử chạy 20 agent trên một refactor lớn hoặc một cuộc di trú (migration) lớn mà không có một mô hình chung, có thể truy vấn được về những gì đã xong và cái gì phụ thuộc vào cái gì, bạn sẽ nhận được công việc trùng lặp, các thay đổi một phần âm thầm không tương thích với nhau, và không có cách nào sạch sẽ để tiếp tục sau một lần thất bại. Một DAG “phát biểu + chứng minh” cho một dự án toán học về mặt chức năng chính là hạ tầng bạn cần cho một DAG “interface + implementation” trong một cuộc di trú code.
Một pattern bạn thực sự có thể mượn
Việc tách statement/proof tổng quát hóa gọn gàng sang điều phối agent phần mềm. Đây là hình dạng của nó áp dụng cho, chẳng hạn, một cuộc di trú type quy mô lớn hoặc refactor API:
# Node DAG đơn giản hóa — "claim" (interface/contract) được theo dõi
# tách biệt khỏi "proof" (implementation), để các agent có thể xây dựng
# dựa trên một contract trước khi implementation hoàn thành.
class MigrationNode:
def __init__(self, name, contract, depends_on=None):
self.name = name
self.contract = contract # "phát biểu" — chữ ký, ràng buộc bất biến
self.implementation = None # "chứng minh" — được điền khi hoàn thành
self.depends_on = depends_on or []
self.description = None # tóm tắt ngôn ngữ tự nhiên để agent tìm kiếm
def is_buildable(self, completed_nodes):
return all(dep in completed_nodes for dep in self.depends_on)
def find_reusable(dag, query_description, embedding_search):
# Trước khi một agent bắt đầu công việc mới, tìm trong mô tả
# của các node hiện có xem đã có gì giải quyết bài toán con này chưa.
return embedding_search(query_description, [n.description for n in dag.nodes])Cơ chế giúp Prove2Me hoạt động không hề kỳ lạ — đó là đồ thị tác vụ nhận biết phụ thuộc cộng với tìm kiếm ngữ nghĩa trên công việc trước đó, thứ mà hầu hết team platform đã có sẵn từng mảnh (build graph, tìm kiếm code). Điều đáng chú ý là điều phối agent cho các tác vụ thực sự chạy dài hạn cần những thứ đó được nối kết tường minh với nhau, thay vì giả định rằng một context window lớn hơn hay một model thông minh hơn sẽ tự lấp đầy khoảng trống.
Điều tôi mang vào công việc nền tảng agent của chính mình
Ba điều từ đây tôi thực sự sẽ áp dụng:
- Phân rã trước khi song song hóa. Hai mươi agent chạy trên một hàng đợi tác vụ không được phân biệt sẽ va chạm nhau. Hai mươi agent chạy trên một DAG với phụ thuộc tường minh và các contract đã được nhận (claimed) nhưng chưa hoàn thành thì không.
- Làm cho công việc dở dang có thể phát hiện được, không chỉ công việc hoàn chỉnh. Pattern “phát biểu không có chứng minh” — công bố một interface trước khi implementation ra đời — cho phép các agent phía sau được unblock ngay lập tức thay vì bị đình trệ hoặc làm trùng lặp.
- Chuẩn bị tinh thần kiến trúc đầu tiên sẽ thất bại với công việc thực sự chạy dài hạn, và dự trù cho một lần thiết kế lại giữa chừng. Chính lần thử chứng minh của Anthropic cần công cụ bên ngoài gắn thêm vào giữa dự án. Nếu một lab với kinh nghiệm điều phối nhiều đến vậy còn đâm vào bức tường đó, hãy lên kế hoạch cho các workload agent chạy dài hạn của chính bạn với giả định rằng bạn sẽ cần thay hạ tầng điều phối ít nhất một lần trước khi nó ổn định — đừng coi thiết kế điều phối đầu tiên của bạn là bản cuối cùng.
Định lý là tiêu đề. Pattern điều phối DAG-các-phát-biểu-và-chứng-minh phía sau nó mới là phần tôi sẽ còn suy nghĩ tới quý sau.