Thomas Hales
hoạt động khoảng năm 1958, San Antonio, Texas, Hoa Kỳ
Nhà toán học người Mỹ chứng minh giả thuyết Kepler về xếp cầu năm 1998 và sau đó dẫn dắt dự án Flyspeck, phiên bản chứng minh hình thức được máy tính kiểm chứng đầy đủ.
Thomas Hales sinh tại San Antonio, Texas, học tại Đại học Stanford và Cambridge, rồi nhận bằng tiến sĩ tại Đại học Princeton năm 1986 dưới sự hướng dẫn của Robert Langlands, nghiên cứu chương trình Langlands. Ông giảng dạy tại Harvard, Đại học Chicago và Viện Nghiên cứu Cao cấp trước khi gia nhập Đại học Michigan năm 1993.
Năm 1998, dựa trên chiến lược do László Fejes Tóth đề xuất năm 1953, Hales cùng nghiên cứu sinh Samuel Ferguson chứng minh giả thuyết Kepler: rằng xếp lập phương tâm mặt và xếp lục giác chặt đạt mật độ xếp cầu đều lớn nhất có thể trong không gian, điều Kepler đã khẳng định năm 1611. Chứng minh kết hợp giải tích cổ điển với khoảng 300 trang lập luận và hàng gigabyte tính toán máy tính đưa bài toán về hàng nghìn trường hợp tối ưu hóa phi tuyến, khiến người phản biện chỉ chắc chắn khoảng 99% về tính đúng đắn sau bốn năm xem xét.
Để xóa bỏ nghi ngờ còn lại, Hales khởi động dự án Flyspeck năm 2003 nhằm kiểm chứng hình thức toàn bộ chứng minh bằng các trợ lý chứng minh HOL Light và Isabelle. Dự án, hoàn thành với một nhóm quốc tế lớn năm 2014 và công bố năm 2017, cho ra chứng minh được máy kiểm tra không còn lỗ hổng — một cột mốc cho toán học có sự trợ giúp của máy tính. Hales là Giáo sư Andrew Mellon tại Đại học Pittsburgh cho đến khi nghỉ hưu vào tháng 5 năm 2025 và tiếp tục nghiên cứu chứng minh hình thức cùng ứng dụng vào các bài toán tối ưu hóa hình học khác.
Nơi làm việc: Đại học Michigan, Đại học Pittsburgh
Hoa Kỳ