MathCode: Trợ lý lập trình AI biến bài toán thường thành chứng minh toán học tự động

MathCode là một trợ lý lập trình AI chạy trên terminal với công cụ hình thức hóa toán học (math formalization engine) tích hợp sẵn. Thay vì chỉ viết code thông thường, công cụ này có thể nhận một bài toán bằng ngôn ngữ tự nhiên, tự động chuyển đổi thành định lý Lean 4 và cố gắng đưa ra một chứng minh chính thức — hoàn toàn tự động.

Với kiến trúc gồm Lean REPL liên tục, thư viện định lý và tiên đề tái sử dụng, cùng khả năng lập luận theo nhiều hướng song song, MathCode hứa hẹn là trợ thủ đắc lực cho các nhà toán học, nhà nghiên cứu AI và lập trình viên muốn chứng minh toán học bằng máy tính.

Giao diện demo MathCode

Tính năng nổi bật

MathCode không chỉ đơn thuần là một mô hình ngôn ngữ lớn hội thoại. Nó được thiết kế như một hệ thống chứng minh toán học tương tác với nhiều lớp chức năng:

• Lean REPL liên tục (Persistent Lean REPL): Máy chủ ngôn ngữ Lean chạy nền, giúp thời gian kiểm tra biên dịch chỉ còn ~0.4 giây sau lần khởi động đầu tiên, thay vì ~30 giây như cách truyền thống.
• Thư viện định lý (Theorem Library): Mỗi định lý chứng minh thành công sẽ được tự động đặt tên, lưu trữ và cho phép tái sử dụng cho các bài toán sau.
• Thư viện tiên đề (Axiom Library): Các giả định trong hội thoại được lưu thành các khai báo Lean bền vững, kiểm tra biên dịch và rà soát tính nhất quán.
• Tích hợp Lean LSP: Tự động tìm kiếm các bổ đề từ Mathlib (thư viện toán học chuẩn của Lean) qua leansearch.net và Loogle, đồng thời dùng chẩn đoán LSP để tự sửa lỗi.
• Đồ thị tri thức Obsidian: Tạo ra một vault Obsidian trực quan hóa mối quan hệ giữa định lý và bổ đề dưới dạng đồ thị tri thức.

Những tính năng prover tiên tiến

Ngoài các khả năng nền tảng, MathCode còn sở hữu các phương pháp chứng minh thông minh:

• Chứng minh theo chế độ tác tử (Agent-Mode Proving): Mỗi chứng minh là một phiên tương tác, nơi AI viết các ứng viên chứng minh, đọc lỗi và biên dịch lại cho đến khi thành công.
• Cây mục tiêu con (Tree-of-Subgoals): Các định lý phức tạp được chia thành những mục tiêu con độc lập, chứng minh song song rồi ghép lại.
• Đa bộ lập kế hoạch (Multi-Planner): Chạy nhiều bộ lập kế hoạch song song để đưa ra các chiến lược chứng minh khác nhau; prover sẽ chọn phương án tối ưu nhất.

Bắt đầu nhanh

MathCode yêu cầu macOS (arm64) hoặc Linux (x86_64), cùng với CLI codex cho backend mặc định. Cài đặt khá đơn giản:

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login
mathcode

Sau khi cài đặt, bạn có thể thử ngay:

mathcode -p "prove that the square of an even number is even"

Kết quả sẽ được ghi vào thư mục LeanFormalizations/. Ngoài ra, bạn cũng có thể chạy giao diện web qua lệnh ./run webui.

Lưu ý: Script setup.sh sẽ chuẩn bị bản release, tải runtime và bộ công cụ Lean, đồng thời cài trình khởi chạy mathcode trên user-local.

So sánh với bối cảnh Việt Nam

Việc nghiên cứu và giảng dạy toán học tại Việt Nam đang có xu hướng chuyển dịch sang ứng dụng công nghệ. Các trường đại học như Đại học Bách Khoa Hà Nội, Đại học Khoa học Tự nhiên TP.HCM đã bắt đầu đưa Lean và các công cụ chứng minh hình thức vào chương trình đào tạo. MathCode, với khả năng tự động hóa cao, có thể là công cụ hữu ích giúp sinh viên và nghiên cứu sinh tiếp cận toán học hiện đại theo cách trực quan hơn.

Tuy nhiên, cộng đồng người dùng MathCode tại Việt Nam còn khá nhỏ. Những ai muốn thử sức nên cân nhắc đầu tư thời gian tìm hiểu về Lean 4 trước — đây là nền tảng kiến thức bắt buộc để sử dụng hiệu quả công cụ này.

Kết luận

MathCode đánh dấu một bước tiến đáng chú ý trong lĩnh vực AI toán học (AI for math), kết hợp giữa khả năng suy luận ngôn ngữ tự nhiên của mô hình ngôn ngữ lớn với sự chính xác tuyệt đối của chứng minh hình thức. Đây không chỉ là một công cụ dành riêng cho giới học thuật, mà còn mở ra cơ hội cho các nhà phát triển xây dựng ứng dụng trên nền tảng toán học xác thực.

Nếu bạn quan tâm đến nghiên cứu về AI, toán học tính toán, hay đơn giản muốn thử một công cụ code mới lạ, MathCode xứng đáng được thêm vào danh sách trải nghiệm.