Lời giải: Flyspeck: chứng minh hình thức của giả thuyết Kepler trong HOL Light và Isabelle (2015)

Một cách xếp là một tập rời rạc vô hạn $V \subset \mathbb{R}^3$ các tâm quả cầu đơn vị, với mọi hai điểm cách nhau ít nhất $2$; mật độ của nó là giới hạn của tỉ lệ không gian mà các quả cầu lấp đầy trong một hộp chứa lớn. Cuốn sách nhỏ "Về bông tuyết sáu cạnh" (1611) của Kepler đưa ra giả thuyết rằng mật độ này không bao giờ vượt quá $\Delta_3 = \pi/\sqrt{18} \approx 0.7405$, giá trị đạt được bởi cách xếp lập phương tâm mặt và bởi vô số cách xếp khác được dựng từ cùng các lớp lục giác. Thomas Hales và Samuel Ferguson chứng minh giả thuyết năm 1998 bằng phân tích trường hợp hình học kết hợp với tính toán máy tính đồ sộ, nhưng theo lời Jeffrey Lagarias, người chủ trì hội đồng phản biện, bản chất của chứng minh "khiến con người khó kiểm tra đáng tin cậy từng bước", và nó được công bố năm 2006 mà không có sự xác nhận đầy đủ.

Phản ứng của Hales, công bố năm 2003, là dự án Flyspeck (Formal Proof of the Kepler conjecture): dựng lại mọi phần của lập luận — cả phần văn bản toán học truyền thống lẫn phần được cài đặt như tính toán máy tính — bên trong hai trợ lý chứng minh HOL Light và Isabelle, để một lõi logic nhỏ, được soi xét kỹ lưỡng kiểm tra từng suy luận thay vì một người phản biện. Dự án kết thúc năm 2014 và bản tường trình chính thức được Hales cùng hai mươi mốt đồng tác giả công bố năm 2017.

Các bước còn lại của bản phác thảo chứng minh này theo đúng dàn ý của bài báo: rút gọn bài toán hình học vô hạn về hữu hạn trường hợp tổ hợp (Bước 2–3), biến phần số học của mỗi trường hợp thành các bất đẳng thức có thể được chứng thực bằng số học thuần túy (Bước 4–7), rồi ghép các mảnh đã chứng thực thành định lý hình thức cuối cùng (Bước 8).