$hide=mobile

Giả Thuyết Kepler Đã Được Chứng Minh Một Cách Hình Thức

Việc một bài toán đã tồn tại 400 năm nay được chứng minh bằng máy tính có thể mở ra một kỷ nguyên mới cho toán học, trong đó máy tính thực hiện các công việc kỹ năng để giải phóng con người cho những suy luận sâu sắc hơn.

Bài toán này là một câu hỏi quen thuộc với những người bán hoa quả ở khắp mọi nơi: Xếp những quả cam thế nào là tốt nhất? Năm 1611, nhà toán học và thiên văn học người Đức Johannes Kepler cho rằng cách sắp xếp theo hình kim tự tháp là hiệu quả nhất, nhưng không thể chứng minh được điều này. 

Johannes Kepler (27/12/1571-15/11/1630)
Suy diễn trực giác của Kepler (mà ngày nay được gọi là giả thuyết Kepler) có thể phát biểu về mặt toán học như sau: Cách thức xếp các khối cầu cùng kích thước trong không gian theo kiểu hình kim tự tháp có mật độ chiếm không gian trung bình lớn nhất trong tất cả các cách xếp. Mật độ trung bình của kiểu √ xếp này có thể tính chính xác là π/3 2. Giả thuyết này là một phần của vấn đề thứ 18 trong danh mục 23 vấn đề nổi tiếng do Hilbert nêu ra năm 1900. Có thể xem cuốn sách [4] để thấy tầm ảnh hưởng của giả thuyết Kepler trong lịch sử toán học.

Gần đây, Thomas Hales, giáo sư của Đại học Pittsburgh, Pennsylvania, thông báo đã hoàn thành một nỗ lực hùng tráng nhằm chứng minh một cách hình thức suy diễn trên của Kepler. Ông nói "Vai tôi đã trút được một gánh nặng khổng lồ" và "Tôi bỗng nhiên cảm thấy trẻ ra mười tuổi!" Tại sao Hales lại nói như vậy và thế nào là một chứng minh hình thức? 

Năm 1998 Hales lần đầu đưa ra chứng minh suy diễn trực giác của Kepler là đúng. Mặc dù có vô hạn cách để xếp các khối cầu, nhưng phần lớn chúng chỉ là biến thể của vài ngàn cấu hình. Hales đã phân chia các khả năng sắp xếp vô hạn khối cầu thành khoảng 2500 cách sắp xếp 50 khối cầu về mặt toán học, rồi sau đó dùng máy tính để kiểm tra mật độ tất cả các cách sắp xếp này. Tuy nhiên đây là một chứng minh khủng khiếp dày 250 trang cùng với 3 gigabytes phần mềm tính toán mà 12 nhà phản biện đã phải mất tới 4 năm để kiểm tra. Cuối cùng tạp chí Annals of Mathematics cũng công bố bài báo của Hales năm 2005 kèm theo một thông báo là các phản biện không thể kiểm tra chứng minh của Hales có đúng hay không. Một tiền lệ chưa từng có! Nhà toán học Gabor Fejes Toth phát biểu rằng chỉ có thể khẳng định "chắc chắn 99 phần trăm" chứng minh là đúng do không thể kiểm chứng được phần tính toán của máy tính. Nhiều nhà toán học không thỏa mãn với chứng minh này của Hales.

Vì vậy, từ năm 2003, Hales bắt đầu chương trình Flyspeck (dựa theo các chữ đầu FPK của câu “Formal Proof of Kepler”), một nỗ lực nhằm xác minh chứng minh của mình là đúng thông qua một sự kiểm chứng hình thức. Điều này có nghĩa là máy tính sẽ kiểm tra các suy luận logic hình thức trong chứng minh có gì sai không. Nhóm nghiên cứu của Hales đã phát triển hai phần mềm trợ giúp chứng minh hình thức có tên gọi là Isabelle và HOL Light. Cả hai phần mềm này đều được xây dựng dựa trên một phần lõi logic đã được kiểm tra kỹ lưỡng là không có bất kỳ lỗi nào. Chúng đưa ra một nền tảng cho phép máy tính có thể kiểm tra bất cứ chuỗi mệnh đề logic nào nhằm xem chúng có đúng không. Có một điều thú vị là ngoài các kiểm chứng độc lập hai phần mềm trên, nhóm của Hales cũng dùng chính hai phần mềm này để tự kiểm tra xem chúng có lỗi không. 

Thomas Callister Hales
Phần đầu tiên của chương trình Flyspeck là phân loại tất cả đồ thị thuần hóa (tame graphs) trong phần mềm Is- abelle được thực hiện bởi Bauer và Nip- kow. Phần này liệt kê cấu trúc tổ hợp của các phản ví dụ tiềm năng cho giả thiết Kepler. Định lý phân loại của họ đã được dịch tương ứng sang phần mềm HOL Light. Phần thứ hai của dự án kiểm tra tính đúng đắn của tất cả các bất đẳng phi tuyến trong HOL dựa trên luận án của Solovyev năm 2012. Việc xác minh tính đúng đắn của tất cả các bất đẳng phi tuyến trong HOL sử dụng thuật toán đám mây Azure của Microsoft trong 5000 giờ. Hầu như tất cả các tính toán được thực hiện song song với 32 lõi, do đó thời gian thực sự là khoảng 5000/32 = 156,25 giờ. Phần cuối cùng của dự án là chứng minh giả thiết Kepler trong HOL Light. Việc xác minh tính đúng đắn của tất cả các chuỗi logic ở mức độ vi mô trong chứng minh giả thiết Kepler bằng phần mềm HOL Light được thực hiện bởi nhóm nghiên cứu Việt Nam trong 6 năm. Nhóm này gồm Triệu Thị Diệp, Đặng Tất Đạt, Vũ Khắc Kỷ, Vương Anh Quyền, Nguyễn Tất Thắng, Trần Nam Trung, Hoàng Lê Trường, Nguyễn Quang Trưởng,... [3]. Trong thời gian đó ông Hales đã nhiều lần đến Viện Toán học tổ chức các bài giảng và hội thảo về chương trình Flyspeck. 

Vào ngày Chủ nhật 10 tháng 8, ngay trước thềm Đại hội Toán học Quốc tế (ICM) 2014, chương trình Flyspeck thông báo họ đã chuyển được chứng minh toán học của Hales sang dạng máy tính và kiểm chứng được rằng nó thực sự chính xác [3]. Tin này lập tức gây chấn động trong cộng đồng toán học. Nhiều tờ báo trên thế giới và Bản tin của ICM 2014 đã đồng loạt đưa tin về sự kiện này

"Công nghệ này loại bỏ các nhà phản biện khỏi quá trình kiểm tra chứng minh”, Hales nói. "Ý kiến của họ về tính chính xác của một chứng minh không còn là vấn đề". "Đó là một nỗ lực to lớn", Alan Bundy của Đại học Edinburgh, Anh, người không tham gia vào công việc này nói. Ông nói thêm rằng ông hy vọng sự thành công của chương trình Flyspeck sẽ khích lệ các nhà toán học khác bắt đầu sử dụng các phần mềm hỗ trợ chứng minh. "Một nhà toán học nổi tiếng thế giới đã sử dụng phép chứng minh định lý một cách tự động. Một sự kiện xã hội như vậy rất quan trọng", ông nói. "Đây là một trường hợp nghiên cứu có thể bắt đầu trở thành tiêu chuẩn." 

Lý tưởng nhất, phần mềm hỗ trợ sẽ làm việc phía sau trong khi các nhà toán học có thể dồn tâm sức cho những ý tưởng mới. Phần mềm đã có thể tự chứng minh một số mệnh đề cơ bản, nhưng nó cần phải dễ dàng sử dụng hơn. "Chúng ta cần biết cách khai thác phép chứng minh để nhận được một bức tranh lớn", Bundy nói. "Việc xem xét mọi thứ ở tầng vi mô vượt quá khả năng của chúng ta. Là con người chúng ta không thể hấp thu quá nhiều." 

Cũng cần nói thêm rằng phương pháp nghiên cứu của Hales đã giúp ông giải quyết được Bài toán tổ ong từ thế kỷ thứ ba trước Công nguyên. Bài toán này nói rằng việc chia một miền phẳng thành các phần có diện tích bằng nhau sẽ có tổng chu vi nhỏ nhất khi chia thành các lục giác đều theo kiểu tổ ong. Ngoài ra, phương pháp của Hales còn có thể có ứng dụng trong việc truyền tín hiệu trong công nghệ thông tin. Thông thường, người ta muốn cùng một lúc gửi đi càng nhiều tín hiệu càng tốt. Tuy nhiên truyền quá nhiều tín hiệu cùng một lúc sẽ gây ra nhiễu. Hales cho rằng “Vấn đề ở đây là mật độ tín hiệu như thế nào là tốt nhất”. Câu hỏi này cũng giống như bài toán xếp khối cầu trong toán học. 

Đối với Hales, ông sẵn sàng để tiếp bước. "Tôi có một cái hộp tràn đầy những ý tưởng mà tôi phải đặt sang một bên khi làm việc với phép chứng minh hình thức này", ông nói. "Chúng ta hãy hy vọng rằng chương trình tiếp theo không mất tới 20 năm!"

Tài liệu tham khảo 

  1. Jacob Aron, Proof confirmed of 400-year-old fruit-stacking problem. New Scientist 12.8.2014. 
  2. Frank Morgan, Kepler’s Conjecture and Hales’s Proof. Notices of the AMS 52(1) (2005), 44-47. 
  3. Flysspeck, Annoucement of completion, https://code.google.com/p/flyspeck/wiki/ An- nouncingCompletion 
  4. George Szpiro, Kepler’s Conjecture: How some of the greatest minds in history helped solve one of the oldest math problems in the world. Wiley & Sons, 2003.

Hoàng Lê Trường

Post a Comment


$hide=home

$type=three$count=6$sr=random$t=oot$h=1$l=0$meta=hide$rm=hide$sn=0

$hide=post$type=three$count=6$sr=random$t=oot$h=1$l=0$meta=hide$rm=hide$sn=0

$hide=home

Kỷ Yếu$cl=violet$type=three$count=6$sr=random$t=oot$h=1$l=0$meta=hide$rm=hide$sn=0

Journals$cl=green$type=three$count=6$sr=random$t=oot$h=1$l=0$meta=hide$rm=hide$sn=0

Name

Ả-rập Xê-út,1,Abel,5,Albania,2,AMM,2,Amsterdam,5,Ấn Độ,1,An Giang,21,Andrew Wiles,1,Anh,2,Áo,1,APMO,19,Ba Đình,2,Ba Lan,1,Bà Rịa Vũng Tàu,52,Bắc Giang,49,Bắc Kạn,1,Bạc Liêu,9,Bắc Ninh,47,Bắc Trung Bộ,7,Bài Toán Hay,5,Balkan,37,Baltic Way,30,BAMO,1,Bất Đẳng Thức,66,Bến Tre,46,Benelux,13,Bình Định,44,Bình Dương,21,Bình Phước,38,Bình Thuận,34,Birch,1,Booklet,11,Bosnia Herzegovina,3,BoxMath,3,Brazil,2,Bùi Đắc Hiên,1,Bùi Thị Thiện Mỹ,1,Bùi Văn Tuyên,1,Bùi Xuân Diệu,1,Bulgaria,5,Buôn Ma Thuột,1,BxMO,12,Cà Mau,13,Cần Thơ,14,Canada,39,Cao Bằng,6,Cao Quang Minh,1,Câu Chuyện Toán Học,36,Caucasus,2,CGMO,10,China,10,Chọn Đội Tuyển,347,Chu Tuấn Anh,1,Chuyên Đề,124,Chuyên Sư Phạm,31,Chuyên Trần Hưng Đạo,3,Collection,8,College Mathematic,1,Concours,1,Cono Sur,1,Contest,610,Correspondence,1,Cosmin Poahata,1,Crux,2,Czech-Polish-Slovak,25,Đà Nẵng,39,Đa Thức,2,Đại Số,20,Đắk Lắk,54,Đắk Nông,7,Đan Phượng,1,Danube,7,Đào Thái Hiệp,1,ĐBSCL,2,Đề Thi HSG,1641,Đề Thi JMO,1,Điện Biên,8,Định Lý,1,Định Lý Beaty,1,Đỗ Hữu Đức Thịnh,1,Do Thái,3,Doãn Quang Tiến,4,Đoàn Quỳnh,1,Đoàn Văn Trung,1,Đống Đa,4,Đồng Nai,49,Đồng Tháp,51,Du Hiền Vinh,1,Đức,1,Duyên Hải Bắc Bộ,25,E-Book,33,EGMO,16,ELMO,19,EMC,8,Epsilon,1,Estonian,5,Euler,1,Evan Chen,1,Fermat,3,Finland,4,Forum Of Geometry,2,Furstenberg,1,G. Polya,3,Gặp Gỡ Toán Học,26,Gauss,1,GDTX,3,Geometry,12,Gia Lai,25,Gia Viễn,2,Giải Tích Hàm,1,Giảng Võ,1,Giới hạn,2,Goldbach,1,Hà Giang,2,Hà Lan,1,Hà Nam,29,Hà Nội,231,Hà Tĩnh,72,Hà Trung Kiên,1,Hải Dương,49,Hải Phòng,42,Hàn Quốc,5,Hậu Giang,4,Hậu Lộc,1,Hilbert,1,Hình Học,33,HKUST,7,Hòa Bình,13,Hoài Nhơn,1,Hoàng Bá Minh,1,Hoàng Minh Quân,1,Hodge,1,Hojoo Lee,2,HOMC,5,HongKong,8,HSG 10,100,HSG 11,86,HSG 12,580,HSG 9,402,HSG Cấp Trường,78,HSG Quốc Gia,99,HSG Quốc Tế,16,Hứa Lâm Phong,1,Hứa Thuần Phỏng,1,Hùng Vương,2,Hưng Yên,32,Hương Sơn,2,Huỳnh Kim Linh,1,Hy Lạp,1,IMC,25,IMO,54,India,45,Inequality,13,InMC,1,International,307,Iran,11,Jakob,1,JBMO,41,Jewish,1,Journal,20,Junior,38,K2pi,1,Kazakhstan,1,Khánh Hòa,16,KHTN,53,Kiên Giang,63,Kim Liên,1,Kon Tum,18,Korea,5,Kvant,2,Kỷ Yếu,42,Lai Châu,4,Lâm Đồng,33,Lạng Sơn,21,Langlands,1,Lào Cai,16,Lê Hải Châu,1,Lê Hải Khôi,1,Lê Hoành Phò,4,Lê Khánh Sỹ,3,Lê Minh Cường,1,Lê Phúc Lữ,1,Lê Phương,1,Lê Quý Đôn,1,Lê Viết Hải,1,Lê Việt Hưng,1,Leibniz,1,Long An,42,Lớp 10,10,Lớp 10 Chuyên,452,Lớp 10 Không Chuyên,229,Lớp 11,1,Lục Ngạn,1,Lượng giác,1,Lương Tài,1,Lưu Giang Nam,2,Lý Thánh Tông,1,Macedonian,1,Malaysia,1,Margulis,2,Mark Levi,1,Mathematical Excalibur,1,Mathematical Reflections,1,Mathematics Magazine,1,Mathematics Today,1,Mathley,1,MathLinks,1,MathProblems Journal,1,Mathscope,8,MathsVN,5,MathVN,1,MEMO,10,Metropolises,4,Mexico,1,MIC,1,Michael Guillen,1,Mochizuki,1,Moldova,1,Moscow,1,Mỹ,9,MYTS,4,Nam Định,32,Nam Phi,1,Nam Trung Bộ,1,National,249,Nesbitt,1,Newton,4,Nghệ An,50,Ngô Bảo Châu,2,Ngô Việt Hải,1,Ngọc Huyền,2,Nguyễn Anh Tuyến,1,Nguyễn Bá Đang,1,Nguyễn Đình Thi,1,Nguyễn Đức Tấn,1,Nguyễn Đức Thắng,1,Nguyễn Duy Khương,1,Nguyễn Duy Tùng,1,Nguyễn Hữu Điển,3,Nguyễn Mình Hà,1,Nguyễn Minh Tuấn,8,Nguyễn Phan Tài Vương,1,Nguyễn Phú Khánh,1,Nguyễn Phúc Tăng,1,Nguyễn Quản Bá Hồng,1,Nguyễn Quang Sơn,1,Nguyễn Tài Chung,5,Nguyễn Tăng Vũ,1,Nguyễn Tất Thu,1,Nguyễn Thúc Vũ Hoàng,1,Nguyễn Trung Tuấn,8,Nguyễn Tuấn Anh,2,Nguyễn Văn Huyện,3,Nguyễn Văn Mậu,25,Nguyễn Văn Nho,1,Nguyễn Văn Quý,2,Nguyễn Văn Thông,1,Nguyễn Việt Anh,1,Nguyễn Vũ Lương,2,Nhật Bản,3,Nhóm $\LaTeX$,4,Nhóm Toán,1,Ninh Bình,41,Ninh Thuận,15,Nội Suy Lagrange,2,Nội Suy Newton,1,Nordic,19,Olympiad Corner,1,Olympiad Preliminary,2,Olympic 10,98,Olympic 10/3,5,Olympic 11,89,Olympic 12,30,Olympic 24/3,6,Olympic 27/4,20,Olympic 30/4,66,Olympic KHTN,6,Olympic Sinh Viên,73,Olympic Tháng 4,12,Olympic Toán,300,Olympic Toán Sơ Cấp,3,PAMO,1,Phạm Đình Đồng,1,Phạm Đức Tài,1,Phạm Huy Hoàng,1,Pham Kim Hung,3,Phạm Quốc Sang,2,Phan Huy Khải,1,Phan Thành Nam,1,Pháp,2,Philippines,8,Phú Thọ,30,Phú Yên,26,Phùng Hồ Hải,1,Phương Trình Hàm,11,Phương Trình Pythagoras,1,Pi,1,Polish,32,Problems,1,PT-HPT,14,PTNK,44,Putnam,25,Quảng Bình,44,Quảng Nam,31,Quảng Ngãi,33,Quảng Ninh,43,Quảng Trị,26,Quỹ Tích,1,Riemann,1,RMM,12,RMO,24,Romania,36,Romanian Mathematical,1,Russia,1,Sách Thường Thức Toán,7,Sách Toán,69,Sách Toán Cao Học,1,Sách Toán THCS,7,Saudi Arabia,7,Scholze,1,Serbia,17,Sharygin,24,Shortlists,56,Simon Singh,1,Singapore,1,Số Học - Tổ Hợp,27,Sóc Trăng,28,Sơn La,11,Spain,8,Star Education,5,Stars of Mathematics,11,Swinnerton-Dyer,1,Talent Search,1,Tăng Hải Tuân,2,Tạp Chí,14,Tập San,6,Tây Ban Nha,1,Tây Ninh,29,Thạch Hà,1,Thái Bình,39,Thái Nguyên,49,Thái Vân,2,Thanh Hóa,57,THCS,2,Thổ Nhĩ Kỳ,5,Thomas J. Mildorf,1,THPT Chuyên Lê Quý Đôn,1,THPTQG,15,THTT,6,Thừa Thiên Huế,35,Tiền Giang,19,Tin Tức Toán Học,1,Titu Andreescu,2,Toán 12,7,Toán Cao Cấp,3,Toán Chuyên,2,Toán Rời Rạc,5,Toán Tuổi Thơ,3,Tôn Ngọc Minh Quân,2,TOT,1,TPHCM,125,Trà Vinh,5,Trắc Nghiệm,1,Trắc Nghiệm Toán,2,Trại Hè,34,Trại Hè Hùng Vương,25,Trại Hè Phương Nam,5,Trần Đăng Phúc,1,Trần Minh Hiền,2,Trần Nam Dũng,9,Trần Phương,1,Trần Quang Hùng,1,Trần Quốc Anh,2,Trần Quốc Luật,1,Trần Quốc Nghĩa,1,Trần Tiến Tự,1,Trịnh Đào Chiến,2,Trung Quốc,12,Trường Đông,19,Trường Hè,7,Trường Thu,1,Trường Xuân,2,TST,55,Tuyên Quang,6,Tuyển Sinh,3,Tuyển Tập,44,Tuymaada,4,Undergraduate,66,USA,44,USAJMO,10,USATST,7,Uzbekistan,1,Vasile Cîrtoaje,4,Vật Lý,1,Viện Toán Học,2,Vietnam,4,Viktor Prasolov,1,VIMF,1,Vinh,27,Vĩnh Long,20,Vĩnh Phúc,63,Virginia Tech,1,VLTT,1,VMEO,4,VMF,12,VMO,46,VNTST,22,Võ Anh Khoa,1,Võ Quốc Bá Cẩn,26,Võ Thành Văn,1,Vojtěch Jarník,6,Vũ Hữu Bình,7,Vương Trung Dũng,1,WFNMC Journal,1,Wiles,1,Yên Bái,17,Yên Định,1,Yên Thành,1,Zhautykov,11,Zhou Yuan Zhe,1,
ltr
item
MOlympiad: Giả Thuyết Kepler Đã Được Chứng Minh Một Cách Hình Thức
Giả Thuyết Kepler Đã Được Chứng Minh Một Cách Hình Thức
https://1.bp.blogspot.com/-gWDX8QKjDAo/WdKP_DvDygI/AAAAAAAAAqA/EXlq_Af2P8wfbiZfw-hDvcRWk0ZC7DRIgCLcBGAs/s1600/Kepler_wide.jpg
https://1.bp.blogspot.com/-gWDX8QKjDAo/WdKP_DvDygI/AAAAAAAAAqA/EXlq_Af2P8wfbiZfw-hDvcRWk0ZC7DRIgCLcBGAs/s72-c/Kepler_wide.jpg
MOlympiad
https://www.molympiad.net/2017/10/gia-thuyet-kepler-uoc-chung-minh-mot-cach-hinh-thuc.html
https://www.molympiad.net/
https://www.molympiad.net/
https://www.molympiad.net/2017/10/gia-thuyet-kepler-uoc-chung-minh-mot-cach-hinh-thuc.html
true
2506595080985176441
UTF-8
Loaded All Posts Not found any posts VIEW ALL Readmore Reply Cancel reply Delete By Home PAGES POSTS View All RECOMMENDED FOR YOU LABEL ARCHIVE SEARCH ALL POSTS Not found any post match with your request Back Home Sunday Monday Tuesday Wednesday Thursday Friday Saturday Sun Mon Tue Wed Thu Fri Sat January February March April May June July August September October November December Jan Feb Mar Apr May Jun Jul Aug Sep Oct Nov Dec just now 1 minute ago $$1$$ minutes ago 1 hour ago $$1$$ hours ago Yesterday $$1$$ days ago $$1$$ weeks ago more than 5 weeks ago Followers Follow THIS PREMIUM CONTENT IS LOCKED Please share to unlock Copy All Code Select All Code All codes were copied to your clipboard Can not copy the codes / texts, please press [CTRL]+[C] (or CMD+C with Mac) to copy