KHOÁ HỌC VỀ

CHỨNG MINH HÌNH THỨC VÀ CHƯƠNG TRÌNH FLYSPECK
 
Thời gian: Từ 8/6/2009 đến 31/7/2009
Địa điểm: Viện Toán học, 18 Hoàng Quốc Việt, Hà Nội
Ban tổ chức: Giáo sư Thomas Hales (Đại học Pittsburgh Hoa Kỳ),
  Tạ Thị Hoài An, Ngô Đắc Tân, Trần Nam Trung (Viện Toán học)
Tổ chức tài trợ: Viện Toán học và Chương trình Flyspeck của Quỹ Khoa học Mỹ.

 

1. Mục đích của Khoá học

Chứng minh hình thức là chứng minh mà mỗi kết luận lôgic được kiểm tra ở mức độ các quy tắc lôgic toán cơ bản. Ngược lại, các chứng minh truyền thống được thực hiện ở mức độ cao hơn. Vì số lượng các bước trong chứng minh hình thức rất lớn nên máy tính thường được sử dụng trong các chứng minh này. Các nhà nghiên cứu làm việc trong lĩnh vực chứng minh hình thức cần được đào tạo cả về toán và về các phần mền tin học chuyên về chứng minh hình thức.

Mục đích chính của Khoá học này là giới thiệu các phương pháp của chứng minh hình thức thông qua các bài giảng. Bài giảng đòi hỏi thực hiện những đóng góp có ý nghĩa cho dự án hình thức hoá. Khoá học cung cấp cho những người mới bắt đầu học các phương pháp của chứng minh hình thức và cũng có các bài giảng chuyên sâu cho những người đã biết cách thực hiện các chứng minh hình thức trên máy vi tính.

 

2. Chương trình Flyspeck

Chương trình Flyspeck là chương trình về chứng minh hình thức lớn nhất hiện nay. Mục đích của chương trình là thực hiện một chứng minh hình thức cho giả thiết xếp mặt cầu (Sphere packings) nổi tiếng của nhà bác học người Đức J. Kepler. Khoá học là dịp để các nhà nghiên cứu của chương trình Flyspeck hiểu nhau hơn.  

Khoá học cũng có các bài giảng về các phương pháp chứng minh hình thức của chương trình Flyspeck. Các bài giảng bao gồm: Lập trình ngôn ngữ OCaml (ngôn ngữ lập trình hàm), phương pháp thực hiện chứng minh hình thức trong HOL Light (một ngôn ngữ dùng để thực hiện các chứng minh hình thức), các phương pháp của giải tích thực, hình học rời rạc, và về chứng minh giả thiết Kepler của Giáo sư Thomas Hales. Khoá học khuyến khích sự hợp tác, trao đổi và giao lưu giữa các những người tham gia từ các nước phát triển với các những người tham gia của Việt Nam và tạo điều kiện cho các nhà nghiên cứu của chương trình Flyspeck cơ hội thảo luận và phát triển các cách tiếp cận mới về chứng minh hình thức cũng như sự hợp tác làm việc trong chương trình. Khoá học cũng bao gồm các các bài giảng về các phương pháp chứng minh hình thức ở nhiều trình độ khác nhau.

 
3. Đăng ký tham gia Khoá học

Đăng ký tham gia Khoá học xin gửi tới địa chỉ:  tntrung@math.ac.vn  hoặc đến dự trực tiếp các bài giảng. Chương trình cụ thể sẽ được thông báo sau.

 
Chương trình làm việc