MathLabs

Phỏng đoán Kepler

Đã giải, 1998Hình họcHilbert #18
Phát biểu

Trong không gian Euclid ba chiều, không cách sắp xếp các quả cầu bằng nhau, không chồng lên nhau nào có mật độ lớn hơn π/18≈0.74048\pi/\sqrt{18} \approx 0.74048 — mật độ của cách xếp lập phương tâm mặt và cách xếp lục giác xếp khít, đúng là cách người bán hàng vẫn chồng cam hay đạn đại bác.

Hales công bố một chứng minh năm 1998 (cùng Samuel Ferguson), kết hợp phép quy giản cổ điển về hữu hạn cấu hình cục bộ với một phép tìm kiếm vét cạn bằng máy tính — kiểm tra các chặn quy hoạch tuyến tính trên khoảng 5.000 trường hợp. Năm 2003, hội đồng mười hai phản biện báo cáo rằng họ "chắc chắn 99%" chứng minh đúng nhưng không thể kiểm tra bằng tay mọi phép tính của máy tính, nên tạp chí Annals of Mathematics vẫn công bố năm 2005 kèm lưu ý đó. Dự án Flyspeck, do Hales dẫn dắt, sau đó xây dựng một chứng minh hình thức đầy đủ, được các trợ lý chứng minh HOL Light và Isabelle kiểm tra từng dòng, xóa bỏ nghi ngờ còn lại; Flyspeck được công bố hoàn tất năm 2014, và chứng minh hình thức được xuất bản năm 2017.

Người giải, 1998Thomas Hales
  1. Flyspeck: chứng minh hình thức của giả thuyết Kepler trong HOL Light và Isabelle (2015)Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller, 2015Độ khó 5/5Nghiên cứuBản tóm lượcCó máy tính hỗ trợ

Tài liệu tham khảo

  1. Thomas C. Hales (2005). A proof of the Kepler conjecture · DOI:10.4007/annals.2005.162.1065
  2. Thomas Hales, Mark Adams, Gertrud Bauer, et al. (2017). A formal proof of the Kepler conjecture · DOI:10.1017/fmp.2017.1
  3. George G. Szpiro (2003). Kepler's Conjecture: How Some of the Greatest Minds in History Helped Solve One of the Oldest Math Problems in the World