Ngày 29-31/07/2026, Viện Nghiên cứu cao cấp về Toán (VIASM) tổ chức Khóa học "Giới thiệu về Chứng minh định lý tự động trong Toán học" (Mini-course: An Introduction to Automatic Theorem-Proving in Mathematics) tại Hà Nội. Khóa học thu hút sự tham gia của các giảng viên, nhà nghiên cứu, nghiên cứu sinh và học viên quan tâm đến chứng minh định lý tự động, hình thức hóa toán học và ứng dụng của các công cụ này trong nghiên cứu khoa học.
Trong bối cảnh các hệ thống trợ lý chứng minh (formal proof assistants) và các mô hình trí tuệ nhân tạo phát triển mạnh mẽ, hình thức hóa toán học đang trở thành một hướng nghiên cứu nhận được nhiều sự quan tâm trên thế giới. Khóa học được thiết kế nhằm cung cấp cho học viên những kiến thức nền tảng về lĩnh vực này, đồng thời giới thiệu các công cụ đang được sử dụng rộng rãi trong cộng đồng toán học quốc tế.
GS.TS. Đào Hải Long (Đại học Kansas, Hoa Kỳ) phát biểu khai mạc Khóa học
Phát biểu khai mạc khóa học, GS.TS. Đào Hải Long, Đại học Kansas, Hoa Kỳ, thành viên Ban Chương trình, nhấn mạnh rằng sự phát triển nhanh chóng của các hệ thống chứng minh định lý tự động và các mô hình trí tuệ nhân tạo đang mở ra những phương thức mới trong nghiên cứu Toán học. Giáo sư cho biết khóa học được xây dựng nhằm giới thiệu những kiến thức nền tảng về hình thức hóa toán học, đồng thời tạo điều kiện để học viên trực tiếp trải nghiệm các công cụ hiện đại đang được sử dụng trong cộng đồng toán học quốc tế. Thông qua các bài giảng và phiên thực hành, học viên không chỉ làm quen với hệ thống Lean và các trợ lý AI hỗ trợ chứng minh mà còn có cơ hội trao đổi, thảo luận về tiềm năng ứng dụng của các công cụ này trong nghiên cứu và giảng dạy Toán học.
TS. Bartosz Naskręcki, Đại học Adam Mickiewicz, Ba Lan giảng bài tại Khóa học
Giảng viên của khóa học, TS. Bartosz Naskręcki, là chuyên gia về lý thuyết số và hình học đại số. Sau khi nhận bằng tiến sĩ tại Đại học Adam Mickiewicz năm 2014, Tiến sĩ đã có nhiều năm nghiên cứu tại Đức, Vương quốc Anh và Ba Lan. Năm 2025, Tiến sĩ tham gia xây dựng FrontierMath, bộ đánh giá các mô hình ngôn ngữ lớn bằng những bài toán toán học có độ khó cao. Tiến sĩ cũng giảng dạy nhiều học phần về mật mã học, tính toán toán học bằng Python và ứng dụng các mô hình ngôn ngữ lớn trong nghiên cứu toán học và lập trình.
Ở phần đầu chương trình, học viên được tìm hiểu các khái niệm cơ bản của lý thuyết kiểu (type theory) – nền tảng của các hệ thống chứng minh hiện đại, cùng tổng quan về các hệ thống chứng minh như Lean, Coq (Rocq), Isabelle và Agda. Bên cạnh đó, giảng viên cũng giới thiệu thư viện Mathlib và phân tích vai trò của Lean trong các dự án hình thức hóa toán học hiện nay.
TS. Bartosz Naskręcki, Đại học Adam Mickiewicz, Ba Lan hướng dẫn học viên thực hành với Lean
Nội dung trọng tâm của khóa học là các phiên thực hành với Lean. Dưới sự hướng dẫn của giảng viên, học viên trực tiếp cài đặt môi trường làm việc, từng bước hình thức hóa một định lý toán học và làm quen với ngôn ngữ tactic của Lean. Khóa học cũng giới thiệu cách khai thác các trợ lý AI như Claude, Codex, Aristotle và Gauss trong quá trình xây dựng chứng minh, đồng thời trao đổi về những lưu ý khi lựa chọn định nghĩa, tổ chức dự án hình thức hóa và phối hợp giữa các nhà nghiên cứu với các công cụ AI.
Các học viên tham dự Khóa học
Thông qua các bài giảng và hoạt động thực hành, khóa học đã giúp học viên bước đầu tiếp cận các phương pháp và công cụ hiện đại trong chứng minh định lý tự động, đồng thời tạo diễn đàn để trao đổi về khả năng ứng dụng các trợ lý AI trong nghiên cứu Toán học và phát triển các dự án hình thức hóa trong thời gian tới.