26/05/2026
AI đang bước vào một giai đoạn mới trong toán học.
Google DeepMind vừa công bố AlphaProof Nexus — một hệ thống dùng mô hình ngôn ngữ lớn kết hợp với Lean, công cụ kiểm chứng chứng minh toán học bằng máy.
Kết quả đáng chú ý: AlphaProof Nexus giải được 9/353 bài toán Erdős mở mà hệ thống đã thử, trong đó có 2 bài đã mở khoảng 56 năm. Ngoài ra, nó còn chứng minh được 44/492 conjecture từ OEIS. Những proof này không chỉ là lời giải dạng văn bản, mà là các chứng minh hình thức có thể được Lean kiểm tra từng bước.
Điểm quan trọng nằm ở chỗ:
AI không chỉ “nói ra một lời giải nghe có vẻ đúng”. Nó phải viết proof trong Lean. Nếu sai, Lean báo lỗi. AI tiếp tục sửa. Chỉ khi proof compile được, không còn phần bỏ trống kiểu sorry, và theorem gốc không bị thay đổi thì kết quả mới được chấp nhận. Paper mô tả rõ cơ chế này: LLM sinh/sửa proof, Lean compiler phản hồi lỗi, rồi agent lặp lại quá trình đó.
Nói đơn giản dễ hiểu thì như sau:
AI đề xuất proof
→ Lean kiểm tra logic
→ sai thì trả lỗi
→ AI sửa tiếp
→ đúng thì proof được xác nhận hình thức
Đây là bước tiến lớn vì điểm yếu lâu nay của LLM trong toán học là ảo giác logic: lời giải có thể rất thuyết phục nhưng sai ở một mắt xích nhỏ. Terence Tao từng cảnh báo rằng AI thường “giỏi tạo cảm giác đúng hơn là thật sự đúng”, và ông cũng nói nếu buộc AI tạo output trong ngôn ngữ được kiểm chứng hình thức thì về nguyên tắc có thể giải quyết phần lớn vấn đề này.
Kevin Buzzard, một trong những người nổi bật trong cộng đồng Lean, cũng nhấn mạnh hướng kết hợp AI với Lean: để AI viết ra output, dịch nó sang Lean, cho Lean kiểm tra, rồi dùng lỗi từ Lean để AI sửa tiếp.
Vì vậy, ý nghĩa thật sự của AlphaProof Nexus không chỉ là “AI giải được 9 bài toán”. Ý nghĩa lớn hơn là nó cho thấy một mô hình làm toán mới đang hình thành:
AI sinh ý tưởng
+ máy kiểm chứng logic
+ con người formalize, định hướng và hiểu ý nghĩa toán học.
P/s: Vài năm trước, cuộc đua chủ yếu là: model nào nói tự nhiên hơn, viết code tốt hơn, làm benchmark cao hơn. Nhưng các tín hiệu gần đây cho thấy xu hướng đang sâu hơn: AI không chỉ sinh văn bản, mà được gắn vào tool, verifier, compiler, proof assistant, simulator, environment để kiểm tra kết quả của chính nó.
