Giả thiết Kepler

Giả thiết Kepler, được đặt theo tên của nhà toán học và nhà thiên văn người Đức Johannes Kepler, là một định lý toán học về xếp hình cầu trong không gian Euclid ba chiều. Nó cho rằng không có sự sắp xếp các quả cầu có cùng kích thước lấp đầy không gian có mật độ trung bình tốt hơn so với việc xếp các khối lập phương (hệ tinh thể lập phương) và sắp xếp các quả cầu giống nhau. Mật độ của sự sắp xếp này chỉ là khoảng 74.05%.
Năm 1998, Thomas Hales đi theo một cách tiếp cận được đề xuất bởi Fejes Tóth vào năm 1953 tuyên bố rằng ông có cách chứng minh giả thiết Kepler. Chứng minh của Hales là chứng minh của sự vắt kiệt bao gồm việc kiểm tra nhiều trường hợp cụ thể, sử dụng các tính toán của máy vi tính phức tạp. Những người đóng vai trò trọng tài đã cho rằng có đến 99% được xác định là đúng trong cách chứng minh của Hales, và giả thiết của Kepler được chấp nhận như một định lý. Năm 2014, đội dự án Flyspeck, được dẫn dắt bởi Hales, đã tuyên bố đã hoàn thiện một chứng minh chính thức của giả thiết Kepler, sử dụng sự kết hợp các trợ thủ Isabelle và HOL Light. Vào năm 2017, chứng minh chính thức đã được chấp nhận bởi Forum of Mathematics.

Nguồn gốc

Giả thiết trên được đề xuất bởi Kepler vào năm 1611 trong một tờ giấy mang tên Bàn về bông tuyết sáu góc. Ông bắt đầu nghiên cứu sự sắp xếp các quả cầu như là một kết quả của sự liên hệ của ông đối với nhà toán học và nhà thiên văn học người Anh Thomas Harriot vào năm 1606. Harriot là người bạn và là trợ thủ của Walter Raleigh, người đã gửi cho Harriot vấn đề làm sao xác định chất những quả pháo thần công trên sàn tàu của ông ấy một cách tốt nhất. Harriot đã xuât bản một tác phẩm về những hình mẫu sắp xếp khác nhau vào năm 1591 và đi đến phát triển phiên bản đầu tiên của lý thuyết nguyên tử .

Thế kỷ 19

Kepler không chứng minh giả thuyết của mình, điều đó chỉ được thực hiện lần đầu tiên bởi Carl Friedrich Gauss vào năm 1831. Gauss đã chứng minh giả thuyết của Kepler là đúng nếu như các quả cầu được sắp xếp trong một mạng lưới thông thường.
Điều đó có nghĩa là bất kỳ sự sắp xếp nào chứng minh giả thiết Kepler là sai là một sự sắp xếp không bình thường. Nhưng loại bỏ tất cả những trường hợp không bình thường đó là rất khó, đó là lý do vì sao giả thiết Kepler rất khó để chứng minh. Thực tế, có những trường hợp không bình thường có mật độ dày đặc hơn xếp khối lập phương một chút vừa đủ, thế nhưng bất kỳ nỗ lực nào để mở rộng sự sắp xếp này để lấp đầy một khoảng trống lớn hơn thì được biết đến ngày nay là giảm mật độ của chính sự sắp xếp đó về mặt thực tế.
Sau Gauss, không có những đi xa hơn để chứng minh giả thiết Kepler trong thế kỷ 19. Vào năm 1900, David Hilbert đã phải thêm giả thiết này vào 23 vấn đề chưa được giải quyết của toán học. Giả thiét là một phần của vấn đề thứ mười tám của Hilbert.

Thế kỷ 20

Việc chứng minh giả thiết Kepler được thúc đẩy bởi László Fejes Tóth. Tóth đã chỉ ra răng vấn đề chỉ ra mật độ lớn nhất của tất cả các sự sắp xếp có thể bị giảm về một con số giới hạn (nhưng rất lớn). Điều đó có nghĩa là chứng minh bằng sự vắt kiệt, về nguyên lý, là có thể. Tóth cũng nhận ra rằng một máy vi tính nhanh vừa đủ có thể biến kết quả lý thuyết thành tiếp cận thực tế cho vấn đề.
Trong khi đó, những nỗ lực để tìm ra con số lớn hơn của mật độ lớn nhất của sự sắp xếp các quả cầu vẫn được thực hiện. Nhà toán học người Anh Claude Ambrose Rogers đã đưa ra giá trị 78% và những nỗ lực tiếp theo của các nhà toán học khác giảm con số này một chút, nhưng vẫn lớn hơn mật độ của sự sắp xếp khối lập phương, khoảng 74%.
Trong năm 1990, Wu-Yi Hsiang tuyên bố đã chứng minh được giả thiết Kepler. Chứng minh này đã được ca ngợi trong Encyclopædia Britannica và Tạp chí Khoa học và Hsiang cũng được ca ngợi trong một cuộc gặp của AMS-MAA. Ông đã sử dụng phương pháp hình học. Tuy nhiên Gábor Fejes Tóth, con trai của László Fejes Tóth, đã nói rằng "Trong những chi tiết được quan tâm, ý kiến của tôi đó là có nhiều điểm mấu chốt không có bằng chứng có thể chấp nhận được". Hales đã gửi lời chỉ trích rất chi tiết vào công trình của Hsiang. Sự đồng thuận hiện tại đó là phương pháp của Hsiang là không chính xác.

Cách chứng minh của Hales

Đi theo cách tiếp cận của Tóth, Thomas Hales, người sau đó làm việc tại Đại học Michigan, đã xác định rằng mật độ lớn nhất của tất cả các sắp xếp có thể được tính ra bằng việc tối thiểu hóa một công thức với 150 biến. Vào năm 1992, với sự hỗ trợ của học trò Samuel Ferguson, Hales giải quyết vấn đề trên chương tình tìm kiếm để ứng dụng có hệ thống quy hoạch tuyến tính để tìm các giá trị nhỏ hơn của giá trị của một công thức, cho mỗi tập hợp của hơn 1500 cấu hình khác nhau của các quả cầu. Nếu giá trị thấp hơn (so với giá trị của công thức) có thể được tìm thấy cho mọi tập hợp của những cấu hình tốt hơn giá trị của công thức cho sự sắp xếp khối lập phương, giả thiết Kepler sẽ được chứng minh. Để tìm giá trị nhỏ hơn cho tất cả các trường hợp, cần phải giải quyết tầm khoảng 100,000 vấn đề quy hoạch tuyến tính.
Khi giới thiệu quá trình thực hiện chương trình vào năm 1996, Hales nói rằng cái kết vẫn còn ở phía trước, nhưng có thể chỉ cần "một đến hai năm" là giải quyết được. Vào tháng 8 năm 1998, Hales đã tuyên bố giả thuyết đã được chứng minh. Vào thời điểm đó, chứng minh gồm 250 trang của ghi chú và 3 gigabyte của chương trình máy tính, dữ liệu và kết quả.
Mặc cho sự thiết tự nhiên của phương pháp, biên tập viên của Annals of Mathematics đã đồng ý xuất bản nó, cung cấp rằng nó được chấp nhận bởi 20 người đứng ra làm trọng tài. Vào năm 2003, sau sự xuất bản đó 4 năm, người đứng đầu của ban trọng tài lúc đó, Gábor Fejes Tóth, đã tuyên bố phương pháp được xác định 99% là chính xác, nhưng có thể nó không được chứng nhận sự chính xác của tất cả các tính toán máy tính.
Sau đó, vào năm 2005, Hales đã xuất bản tài liệu gồm 100 trang mô tả chi tiết phần không được thực hiện bằng máy tính của chứng minh của ông. Vào năm 2006, cả Hales và Ferguson đã cho xuất bản một tài liệu khác, cùng với đó là các tài liệu tiếp theo mô tả phần máy tính thực hiện của chứng minh. Cuối cùng, cả Hales và Ferguson nhận Giải Fulkerson vào năm 2009 cho việc giải quyết các vấn đề toán học không cần giấy tờ.

Chứng minh chính thức

Vào tháng 1 năm 2003, Hales đã tuyên bố một dự án hợp tác để cho ra đời phương pháp chứng minh hoàn thiện cho giả thuyết Kepler. Mục tiêu là loại bỏ bất kỳ sự không chắc chắn về khả năng đúng đắn của chứng minh bằng việc xây dựng một chứng minh chính thức có thể được xác minh bằng kiểm tra chứng minh tự động như các phần mêm HOL Light và Isabelle. Dự án mang tên Flyspeck, các chữ F, P và K là viết tắt của Former Proof of Kepler (Chứng minh chính thức của Kepler). Hales ước tính việc đưa ra một chứng minh chính thức hoàn toàn có thể mất khoảng 20 năm. Hales lần đầu xuất bản một bản thiết kế cho chứng minh chính thức vào năm 2012, dự án được tuyên bố đã hoàn thành vào ngày 10 tháng 8 năm 2014. Vào tháng 1 năm 2015, Hales và 21 cộng sự đã nộp một tài liệu mang tên Chứng minh chính thức cho giả thiết Kepler cho arXiv, tuyên bố rằng đã chứng minh được giả thiết. Vào năm 2017, phương pháp chính thức đã được chấp nhận bởi tạp chí Forum of Mathematics.