Giả thuyết Kepler

Giả thuyế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.

Hoàn cảnh

Mô phỏng xếp khối lập phương (trái) và xếp khối sáu mặt (phải).

Tưởng tượng việc lấp đầy một khoảng trống với những quả cầu có cùng kích thước nhỏ. Mật độ của việc sắp xếp là như nhau cho mức độ tập hợp của những quả cầu được phân chia bởi lượng của vật chứa. Tăng lớn nhất có thể số quả cầu đó có nghĩa là có một sự sắp xếp với mật độ lớn nhất có thể, vì thế các quả cầu được sắp xếp gần nhất có thể.

Thí nghiệm chỉ ra rằng thả những quả cầu một cách ngẫu nhiên sẽ đạt được mật độ lấp đầy là khoảng 65%. Tuy nhiên, một mật độ lớn hơn có thể đạt được nếu các quả cầu được sắp xếp một cách cẩn thận. Bắt đầu với một lớp các quả cầu trong lưới lục giác, sau đó đặt một lớp tiếp theo ở điểm thấp nhất bạn có thể đặt ở trên lớp đầu tiên, và cứ tiếp tục như vậy. Ở mỗi bước như thế có hai lựa chọn để đặt các lớp quả cầu, và giải pháp tự nhiên sẽ tạo ra một số vô hạn không thể đếm được của các lớp, những cách sắp xếp tốt nhất là xếp khối lập phương và xếp lục giác. Mỗi sự sắp xếp này có mật độ trung bình là:

${\frac {\pi }{3{\sqrt {2}}}}=0.740480489\ldots$

Giả thiết Kepler đã cho rằng đó là mật độ tốt nhất mà chúng ta có thể đạt được. Các cách sắp xếp khác không cho mật độ cao hơn.

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.

Những vấn đề liên quan

• Giả thiết Thue
• Giả thiết tổ ông lục giác
• Giả thiết khối mười hai mặt
• Vấn đề Kelvin
• Sắp xếp các quả cầu trong các mật độ cao hơn
• Giả thiết sắp xếp Ulam

Tham khảo

• Aste, Tomaso; Weaire, Denis (2000), The pursuit of perfect packing, Bristol: IOP Publishing Ltd., doi:10.1887/0750306483, ISBN 978-0-7503-0648-5, MR 1786410
• Gauss, Carl F. (1831), “Untersuchungen über die Eigenschaften der positiven ternären quadratischen Formen von Ludwig August Seber”, Göttingische gelehrte Anzeigen
• Hales, Thomas C. (2005), “A proof of the Kepler conjecture”, Annals of Mathematics, Second Series, 162 (3): 1065–1185, arXiv:math/9811078, doi:10.4007/annals.2005.162.1065, ISSN 0003-486X, MR 2179728
• Hales, Thomas C. (2000), “Cannonballs and honeycombs”, Notices of the American Mathematical Society, 47 (4): 440–449, ISSN 0002-9920, MR 1745624 An elementary exposition of the proof of the Kepler conjecture.
• Hales, Thomas C. (1994), “The status of the Kepler conjecture”, The Mathematical Intelligencer, 16 (3): 47–58, doi:10.1007/BF03024356, ISSN 0343-6993, MR 1281754
• Hales, Thomas C. (2006), “Historical overview of the Kepler conjecture”, Discrete & Computational Geometry, 36 (1): 5–20, doi:10.1007/s00454-005-1210-2, ISSN 0179-5376, MR 2229657
• Hales, Thomas C.; Ferguson, Samuel P. (2006), “A formulation of the Kepler conjecture” (PDF), Discrete & Computational Geometry, 36 (1): 21–69, arXiv:math/9811078, doi:10.1007/s00454-005-1211-1, ISSN 0179-5376, MR 2229658
• Hales, Thomas C.; Ferguson, Samuel P. (2011), The Kepler Conjecture: The Hales-Ferguson Proof, New York: Springer, ISBN 978-1-4614-1128-4
• Hales, Thomas C. (2012), “Dense Sphere Packings: A Blueprint for Formal Proofs”, London Mathematical Society Lecture Note Series, Cambridge University Press, 400, ISBN 978-0-521-61770-3
• Henk, Martin; Ziegler, Guenther (2008), La congettura di Keplero, La matematica. Problemi e teoremi, 2, Torino: Einaudi
• Hsiang, Wu-Yi (1993), “On the sphere packing problem and the proof of Kepler's conjecture”, International Journal of Mathematics, 4 (5): 739–831, doi:10.1142/S0129167X93000364, ISSN 0129-167X, MR 1245351
• Hsiang, Wu-Yi (1995), “A rejoinder to T. C. Hales's article: ``The status of the Kepler conjecture”, The Mathematical Intelligencer, 17 (1): 35–42, doi:10.1007/BF03024716, ISSN 0343-6993, MR 1319992
• Hsiang, Wu-Yi (2001), Least action principle of crystal formation of dense packing type and Kepler's conjecture, Nankai Tracts in Mathematics, 3, River Edge, NJ: World Scientific Publishing Co. Inc., doi:10.1142/9789812384911, ISBN 978-981-02-4670-9, MR 1962807
• Kepler, Johannes (1611), Strena seu de nive sexangula (The six-cornered snowflake), ISBN 978-1-58988-053-5, MR 0927925, tóm lược dễ hiểu
• Hales, Thomas C.; MacLaughin, Sean (2010), “The dodecahedral conjecture”, Journal of the American Mathematical Society, 23 (2): 299–344, arXiv:math.MG/9811079, Bibcode:2010JAMS...23..299H, doi:10.1090/S0894-0347-09-00647-X
• Marchal, Christian (2011), “Study of Kepler's conjecture: the problem of the closest packing”, Mathematische Zeitschrift, 267 (3–4): 737–765, doi:10.1007/s00209-009-0644-2
• Rogers, C. A. (1958), “The packing of equal spheres”, Proceedings of the London Mathematical Society, Third Series, 8 (4): 609–620, doi:10.1112/plms/s3-8.4.609, ISSN 0024-6115, MR 0102052
• Szpiro, George G. (2003), Kepler's conjecture, New York: John Wiley & Sons, ISBN 978-0-471-08601-7, MR 2133723
• Fejes Tóth, L. (1953), Lagerungen in der Ebene, auf der Kugel und im Raum, Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, Band LXV, Berlin, New York: Springer-Verlag, MR 0057566

Liên kết ngoài

• Weisstein, Eric W., "Kepler Conjecture" từ MathWorld.
• Front page of 'On the six-cornered snowflake'
• Thomas Hales' home page Lưu trữ 2009-01-31 tại Wayback Machine
• Flyspeck project home page
• Overview of Hales' proof Lưu trữ 2011-09-27 tại Wayback Machine
• Article in American Scientist by Dana Mackenzie
• Flyspeck I: Tame Graphs, verified enumeration of tame plane graphs as defined by Thomas C. Hales in his proof of the Kepler Conjecture