Toán học thời 4.0

diễn đàn khoa học - công nghệ<br /> Diễn đàn Khoa học - Công nghệ<br /> <br /> <br /> <br /> Toán học thời 4.0<br /> GS Hà Huy Khoái<br /> Trường Đại học Thăng Long<br /> <br /> <br /> “Nghề làm toán trong thời đại 4.0” có thể sẽ rất khác với những gì vẫn được hiểu hàng ngàn năm nay.<br /> Cuộc cách mạng công nghiệp lần thứ 4 không chỉ tạo ra làn gió mới, mà thậm chí là “cơn bão” trong<br /> toán học, kéo theo nó, không chỉ là hứng khởi, hân hoan, mà còn cả sự nghi ngờ, tranh cãi.<br /> Những vấn đề cốt lõi lại một lần nữa được đặt ra: thế nào là “chân lý toán học”, thế nào là một “chứng<br /> minh”? Bài viết giới thiệu với bạn đọc một số vấn đề xuất hiện khi sử dụng máy tính trong chứng<br /> minh toán học, và hơn nữa, trong việc thay thế dần lao động của nhà toán học.<br /> Chứng minh toán học vào trực giác. đưa ra một số ví dụ về sai lầm của<br /> các nhà toán học.<br /> Vào thế kỷ VI và VII TCN, các học Bỏ qua nhiều lập luận logic trung<br /> giả Hy Lạp đã đưa ra cái mà về sau gian nghĩa là trong các lập luận, nhà Với những định lý mà chứng minh<br /> gọi là suy luận logic: đó là chuỗi các toán học luôn dừng lại ở mức mà tương đối ngắn, người ta có thể kiểm<br /> suy luận - các phép tam đoạn luận người đọc “hiểu được”. Chính vì thế tra từng dòng chứng minh để bảo<br /> - chúng buộc người đối thoại chấp mà trong công việc của thầy giáo đảm những lập luận trung gian đã<br /> nhận khẳng định Q một khi đã đồng toán, một phần lớn là làm cho học bị bỏ qua thực sự là đúng đắn. Tuy<br /> ý một khẳng định P trước đó. Ta biết sinh hiểu được những lập luận logic nhiên điều này không dễ khi chứng<br /> rằng, từ thế kỷ thứ V TCN, các nhà trung gian đã bị bỏ qua trong chứng minh dài khoảng 100 trang, hay hơn<br /> tư tưởng Hy Lạp đã là những bậc minh. Mặt khác, các yếu tố trực giác nữa. Đặc biệt, với những chứng minh<br /> thầy về nghệ thuật sắp xếp lý luận thường được sử dụng, nhất là trong có sự trợ giúp của máy tính thì tính<br /> thành một chuỗi liên tiếp các kết luận các chứng minh hình học, và cả trong đúng đắn của nó là điều không dễ<br /> logic, điều này được thấy rõ trong các những lĩnh vực toán học hiện đại như chấp nhận. Đặc điểm chung của<br /> tác phẩm của những nhà ngụy biện, Tô pô. Các nhà toán học sử dụng những chứng minh có trợ giúp của<br /> cũng như trong các đoạn đối thoại trực giác để làm ngắn gọn trình bày máy tính là: bằng những lập luận<br /> của Platon. Họ khám phá ra rằng, chứng minh, và tất nhiên khi cần, họ toán học, người ta đưa bài toán về<br /> những lý luận này có thể lấy bất cứ phải có lập luận logic chặt chẽ mà việc kiểm tra hữu hạn trường hợp.<br /> hoạt động nào của con người làm đối không viện đến trực giác. Tuy nhiên, trong nhiều chứng minh,<br /> tượng, đặc biệt là những công thức số hữu hạn trường hợp này là quá<br /> Với việc bỏ qua một số lập luận<br /> toán học và hình học, hầu hết trong lớn, đến nỗi người ta khó có thể tin<br /> logic và sự tham gia của trực giác,<br /> số đó đến từ nền văn minh Ai Cập hoàn toàn vào công việc của máy<br /> vấn đề đặt ra là: các định lý toán học<br /> và Babylon. Những lý luận này trở tính. Sự tranh luận trong giới toán học<br /> có đáng tin cậy hay không? Chúng<br /> thành chứng minh kết nối những định về việc có thể xem chứng minh với sự<br /> ta thường tin và sử dụng trong công<br /> lý với nhau. Những chứng minh đầu trợ giúp của máy tính là một chứng<br /> việc của mình những định lý mới,<br /> tiên được tìm thấy trong Analytica minh hay không trở nên đặc biệt sôi<br /> những kết quả mới của toán học,<br /> Posteriora của Aristotle, theo đó, các nổi sau khi xuất hiện chứng minh của<br /> nếu đó là kết quả của nhà toán học<br /> định lý được suy ra từ một chuỗi lập Bài toán 4 màu.<br /> “có uy tín”, và đăng tải trên những<br /> luận mà người đọc hiểu được không<br /> tạp chí “đáng tin cậy”. Tuy nhiên, rõ<br /> cần giải thích gì thêm, và một số tiên Bài toán 4 màu và chứng minh hình thức<br /> ràng điều này không đảm bảo tuyệt<br /> đề được chấp nhận. Có thể dễ dàng chứng minh rằng,<br /> đối cho sự đúng đắn của các định lý<br /> Chứng minh toán học theo hình đó. Nhà toán học nào cũng có thể với mọi bản đồ tuỳ ý, ta có thể dùng<br /> mẫu của Aristotle và Euclid có hai sai lầm khi bỏ qua các lập luận logic 5 màu để tô, mỗi nước một màu, sao<br /> đặc điểm nổi bật là bỏ qua nhiều suy trung gian, và người duyệt đăng cũng cho hai nước có chung phần biên giới<br /> luận logic trung gian và dựa nhiều vậy. Trong bài này, chúng tôi cũng sẽ sẽ được tô bởi hai màu khác nhau.<br /> <br /> <br /> <br /> 4<br /> Soá 4 naêm 2019<br />  Diễn đàn khoa học - công nghệ<br /> <br /> <br /> Năm 1852, Francis Guthrie đưa ra nhận rằng, bài toán 4 màu đã được triển mạnh mẽ trong những năm gần<br /> giả thuyết rằng, có thể dùng 4 màu giải. đây của lý thuyết chứng minh và<br /> để tô bản đồ tuỳ ý với yêu cầu hai kiểm tra tự động. Xa hơn nữa, toán<br /> Năm 1996, Robertson, Sanders,<br /> nước có phần biên giới chung phải có học đang đứng trước một mục tiêu rất<br /> Seymour và Thomas tiến một bước<br /> màu khác nhau. Giả thuyết trên được “lãng mạn”: sẽ đến lúc máy tính có<br /> dài khi công bố công trình “Một<br /> Cayley phát biểu chính thức vào năm thể thay thế con người trong lao động<br /> chứng minh mới của Định lý 4 màu”,<br /> 1878, và nổi tiếng với tên gọi Bài toán toán học.<br /> trong đó phần lập luận toán học còn<br /> 4 màu. Sau đó, Bài toán 4 màu đã Điều khác biệt giữa việc “kiểm tra”<br /> khoảng 20 trang, và viết chương trình<br /> nhận được rất nhiều “chứng minh”, của máy và người là gì? Người phản<br /> trên ngôn ngữ C để kiểm tra trên các<br /> và rồi lại được chỉ ra “chứng minh” biện một bài báo gửi đến tạp chí sẽ<br /> lớp đồ thị cụ thể, mà số lượng của<br /> là sai, kể cả chứng minh của một số chấp nhận khâu nào đó của chứng<br /> chúng từ 1.478 được rút xuống còn<br /> nhà toán học nổi tiếng. Xin kể ra đây minh trong bài báo là đúng khi thấy<br /> 633. Có thể tin vào chứng minh của<br /> vài ví dụ: nó “hiển nhiên đúng”. Mức độ “hiển<br /> họ được không? Nếu cho rằng 20<br /> - Năm 1879, Kempe công bố một trang lập luận toán học có thể kiểm nhiên” này phụ thuộc rất nhiều vào<br /> chứng minh. tra kỹ lưỡng thì có gì đảm bảo chương trình độ của người thẩm định. Máy<br /> trình máy tính được viết chính xác? tính không như vậy: “nó” chỉ chấp<br /> - Năm1880, Tait công bố một<br /> Và có gì đảm bảo máy tính chạy nhận một kết luận là đúng nếu mọi<br /> chứng minh khác.<br /> trong nhiều giờ (hàng ngàn giờ) để suy luận logic đều được trình bày,<br /> - Năm 1890, Heawood chỉ ra cái kiểm tra mà không gặp sai sót? dẫn dắt từ những chân lý đầu tiên, tức<br /> sai trong chứng minh của Kempe (11 là các tiên đề.<br /> Trên thực tế, người ta thấy rằng,<br /> năm sau khi chứng minh được công<br /> trung bình cứ một dòng lệnh thì người Để làm ví dụ, ta thử xem máy tính<br /> bố).<br /> lập trình mắc 1,5 lỗi. Nói chung các chứng minh “1+1=2” như thế nào:<br /> - Năm 1891, Petersen phát hiện lỗi này được lập trình viên kiểm tra và 1+1=1+S(0)=S(1+0)=S(1)=2, ở đây<br /> chứng minh của Tait cũng sai! sửa chữa ngay, nhưng trong bản cuối S là ký hiệu “phần tử đi liền sau”<br /> cùng, trung bình cứ 100 dòng lệnh thì trong hệ tiên đề số học của Peano,<br /> Năm 1976, một sự kiện gây xôn<br /> có 1 lỗi chưa được chữa. Thường thì và các phép tính thực hiện theo các<br /> xao giới toán học: Appel và Haken<br /> các lỗi nhỏ không để lại ảnh hưởng gì quy định về quan hệ giữa phép cộng<br /> công bố chứng minh Giả thuyết 4<br /> lớn trong ứng dụng, và lỗi được xem và “đi liền sau”.<br /> màu, một chứng minh có sự trợ giúp<br /> là một phần trong “văn hoá lập trình”!<br /> của máy tính. Có thể tóm tắt chứng Trong chứng minh trên, không<br /> Tuy nhiên, có một số lỗi trong lập<br /> minh của Appel và Haken như sau: có lập luận nào bị bỏ qua, không có<br /> trình dẫn đến hậu quả nghiêm trọng,<br /> trước tiên, ta đưa bài toán 4 màu về chỗ nào dựa vào trực giác. Tiếc rằng,<br /> như vụ nổ của tàu vũ trụ Ariane 5 tốn<br /> bài toán trên đồ thị. Mỗi nước được các định lý khác không đơn giản như<br /> hàng trăm triệu USD. Shamir, một<br /> thay bởi một đỉnh của đồ thị, hai đỉnh “1+1=2”, và để quay về đến tận các<br /> trong ba người sáng lập hệ mã RSA,<br /> của đồ thị được nối bởi một cạnh tiên đề, một định lý đơn giản có thể<br /> có lần phát biểu trên New York Times<br /> khi và chỉ khi hai nước tương ứng có cần đến hàng chục ngàn dòng lệnh.<br /> rằng: một lỗi nhỏ về toán trong con<br /> chung một phần biên giới. Như vậy, Chính vì thế mà khi nhóm Bourbaki<br /> chip sử dụng rộng rãi có thể dẫn đến<br /> giả thuyết 4 màu được đưa về giả đặt cho mình nhiệm vụ xây dựng lại<br /> sai sót trong mã hoá, và đặt an ninh<br /> thuyết sau: có thể dùng 4 màu để cơ sở toán học, họ đã nói là không<br /> thương mại toàn cầu vào tình trạng<br /> tô các đỉnh của một đồ thị phẳng tuỳ nhằm mục tiêu dẫn đến các chứng<br /> nguy hiểm.<br /> ý, sao cho hai đỉnh kề luôn có màu minh hình thức, vì nó đòi hỏi dung<br /> khác nhau. Như vậy, không thể hoàn toàn lượng quá lớn cho mỗi chứng minh.<br /> tin vào những chứng minh của các<br /> Bằng những lập luận toán học, Lý thuyết chứng minh hình thức<br /> nhà toán học, vì họ có thể sai. Cũng<br /> Appel và Haken đưa bài toán tổng (formal proof) có mục tiêu nhờ máy<br /> không thể hoàn toàn tin vào các<br /> quát trên về việc kiểm tra trên 1.478 tính làm thay con người cái công<br /> chứng minh có sự trợ giúp của máy<br /> đồ thị cụ thể. Phần “lập luận toán việc nhọc nhằn là kiểm tra từng khâu<br /> tính, vì chương trình có thể mắc lỗi,<br /> học” dài hơn 1.000 trang, và để kiểm chứng minh. Vấn đề là làm sao cho<br /> máy tính có thể hoạt động sai! Làm<br /> tra 1.478 đồ thị, cần phải viết chương máy tính “hiểu” được ngôn ngữ toán<br /> thế nào để có thể đạt được sự tin cậy<br /> trình máy tính. Liệu có thể tin vào học, từ đó có thể kiểm tra từng khâu<br /> cao nhất vào các kết quả toán học?<br /> một chứng minh như thế hay không? chứng minh xem có lập luận nào mâu<br /> Phần lớn các nhà toán học chưa thừa Vấn đề nêu trên dẫn đến sự phát thuẫn hoặc có lập luận nào đã bị bỏ<br /> <br /> <br /> <br /> 5<br /> Soá 4 naêm 2019<br /> Diễn đàn Khoa học - Công nghệ<br /> <br /> <br /> trống. Chứng minh hình thức là một với chứng minh hình thức, chúng ta Đây là trường hợp hiếm hoi, khi một<br /> phần trong lĩnh vực rộng lớn hơn, là sẽ bắt đầu bằng một sự kiện gây xôn bài báo được đăng mà những người<br /> tự động hoá quá trình tư duy toán xao giới toán học năm 1998: Thomas phản biện không dám tin chắc 100%<br /> học, từ phát hiện giả thuyết đến xây Hales chứng minh Giả thuyết Kepler chứng minh trong bài báo là đúng!<br /> dựng lý thuyết. (tồn tại đã 400 năm). Tuy nhiên, cũng cần lưu ý rằng, công<br /> trình được đăng sau 9 năm, kể từ khi<br /> Thực ra, ý tưởng xây dựng toàn Năm 1611 Thomas Harriot hỏi<br /> Kepler rằng làm cách nào để xếp nó được gửi đến toà soạn.<br /> bộ toán học như một ngôn ngữ hình<br /> thức đã có từ lâu, đặc biệt là khi các viên đạn đại bác hình cầu sao Thomas Hales không bằng lòng<br /> Hilbert khởi xướng chủ nghĩa hình cho đảm bảo xếp được nhiều nhất. với việc công trình của mình chỉ được<br /> thức (formalism) trong toán học, Kepler đưa ra giả thuyết: tốt nhất là “tin là đúng”, mà chưa được kiểm tra<br /> với mục tiêu đưa toán học vượt qua xếp như các bà bán cam ngoài chợ, trọn vẹn. Ông quyết định nhờ máy<br /> những khủng hoảng trong cơ sở của tức là bắt đầu xếp một lớp quả cầu tính kiểm tra, vì chỉ có máy tính mới<br /> lý thuyết tập hợp Cantor. Tham vọng trong lưới lục giác, sau đó đặt một lớp có thể tiến hành công việc nhọc nhằn<br /> của Hilbert là hình thức hoá toàn bộ tiếp theo ở điểm thấp nhất mà bạn có đó. Để kiểm tra chứng minh của<br /> toán học, xuất phát từ các tiên đề và thể đặt bên trên lớp đầu tiên, và cứ mình về tính đúng đắn của giả thuyết<br /> các quy tắc logic, khi đó định lý sẽ tiếp tục như vậy. Kepler, Hales xây dựng một đề án lấy<br /> là một mệnh đề “đúng ngữ pháp”. tên là Flyspeck, gợi ý từ ba chữ FPK<br /> Tuy nhiên, chương trình của Hilbert (Formal proof of Kepler Conjecture).<br /> sụp đổ sau khi xuất hiện công trình Dự án này kết thúc vào năm 2014, và<br /> nổi tiếng của Goedel: định lý về như vậy, chứng minh của Hales được<br /> tính không đầy đủ (incompleteness kiểm tra đầy đủ.<br /> theorem, còn gọi là định lý bất toàn).<br /> Tuy nhiên, có thể tin được hay<br /> Theo định lý Goedel, một hệ tiên đề<br /> không vào “sự kiểm tra” đó? Nói<br /> phi mâu thuẫn thì sẽ không đầy đủ,<br /> cách khác, cần kiểm tra tính đúng<br /> tức là luôn tồn tại những mệnh đề<br /> đắn của việc kiểm tra chứng minh<br /> không thể chứng minh hay bác bỏ<br /> bằng máy tính! Khi xây dựng đề<br /> nếu chỉ sử dụng những lập luận nội<br /> án của mình, Hales dùng hệ HOL<br /> tại của hệ tiên đề đó. Hệ quả hiển<br /> Light (Lightweight implementation of<br /> nhiên của nó là không thể hình thức<br /> Higher Order Logic). HOL Light vừa<br /> hoá toàn bộ toán học.<br /> là một hệ tiên đề toán học, vừa là một<br /> Mặc dù không thể đạt được mục Cách xếp này cho mật độ sử dụng chương trình máy tính. Phần quan<br /> tiêu cuối cùng, nhưng chủ nghĩa hình không gian tối ưu, khoảng trọng nhất trong HOL Light là những<br /> thức của Hilbert đã mang lại diện mạo dòng lệnh liên quan các tiên đề và<br /> mới cho toán học. Các lý thuyết toán các quy tắc logic, gọi là hạt nhân<br /> học trở nên chặt chẽ hơn, và nhiều Thomas Hales đưa ra một chứng của hệ thống. Mỗi một lỗi trong hạt<br /> hệ chứng minh hình thức ra đời. Nổi minh rất khó kiểm tra: chứng minh nhân có thể dẫn đến sai lầm thảm<br /> tiếng nhất là các hệ Coq, HOL Light, của ông bao gồm 300 trang lập luận họa của cả hệ thống. Chẳng hạn,<br /> Isabelle. Người ta xây dựng được toán học và chương trình tính toán một tiên đề được viết sai có thể phá<br /> nhiều chứng minh hình thức cho khoảng 50.000 dòng lệnh! Năm vỡ tính phi mâu thuẫn của hệ thống.<br /> những định lý nổi tiếng của toán học, 1996, ông gửi công trình của mình Rất may, hạt nhân này chỉ chiếm 500<br /> như Định lý về tính không đầy đủ của đến tạp chí toán học uy tín nhất là dòng lệnh, và như vậy có thể kiểm tra<br /> Goedel (1986), Luật thuận nghịch Annals of Mathematics. Toà soạn kỹ lưỡng để tin rằng trong hạt nhân<br /> toàn phương của Gauss (1990), phải làm một việc chưa từng có: nhờ không có lỗi. Tuy nhiên kinh nghiệm<br /> Định lý cơ bản của giải tích (1996), 12 người phản biện. Các phản biện sử dụng các hệ chứng minh hình<br /> Định lý cơ bản của đại số (2000), Bài tiến hành seminar trong 9 năm trời thức cho thấy đối với mỗi hệ, người<br /> toán 4 màu (2004), Định lý điểm bất để kiểm tra, và không tìm thấy một ta tìm ra lỗi sau khoảng 10-15 năm<br /> động Brouwer (2005), Định lý đường sai sót nào. Tuy nhiên họ thừa nhận sử dụng.<br /> cong Jordan (2005), Định lý thặng dư là không thể đủ sức kiểm tra toàn bộ, Mặt khác, theo định lý Goedel,<br /> Cauchy (2007), Định lý số nguyên tố và đề nghị toà soạn đăng vì “tin rằng mỗi hệ chứng minh hình thức không<br /> (2008), Giả thuyết Kepler (2014). chứng minh là hoàn toàn đúng”! Bài thể “tự mình” kiểm tra được chân lý.<br /> Để làm rõ một số vấn đề đặt ra đối báo của Hales được đăng năm 2005. Để khắc phục điều đó, người ta dùng<br /> <br /> <br /> <br /> 6<br /> Soá 4 naêm 2019<br />  Diễn đàn khoa học - công nghệ<br /> <br /> <br /> hệ hình thức này để kiểm tra tính suy luận logic để tạo ra con đường ý định vượt qua mọi giới hạn của tri<br /> đúng đắn của hệ hình thức khác. Giả nối từ giả thiết đến kết luận, thông thức thì chỉ còn cách dựa vào máy<br /> sử mỗi hệ hình thức có xác suất sai qua những định lý đã có sẵn. Xuất tính. Sẽ đến ngày tri thức nhân loại<br /> lầm p, thì khi kiểm tra một hệ nào đó phát từ các giả thiết, nhà toán học bắt được lưu giữ trong hệ thống máy tính,<br /> bằng cách sử dụng n hệ khác, ta có đầu vận dụng những kiến thức mà và thỉnh thoảng máy sẽ cho ta những<br /> thể đưa xác suất sai lầm đến pn. Với mình có được, bổ sung thêm những tri thức mà ta không thể biết chúng từ<br /> n đủ lớn thì xác suất này gần bằng 0. kiến thức mới cần thiết, và từ đống đâu ra, tức là không biết chúng được<br /> “hỗn độn” đó, tìm ra con đường đi cần “chứng minh” như thế nào.<br /> Những lập luận trên đây chỉ ra<br /> rằng, những chân lý toán học, nếu thiết. Thật khó chấp nhận cái ngày mà<br /> không phải là quá phức tạp, thì dù Làm thế nào để máy tính thực máy tính cho ta các lý thuyết toán học<br /> được chứng minh chỉ bởi các nhà toán hiện được công việc nêu trên của nhà mới, các kết quả mới, mà chỉ “nó” biết<br /> học, hay có sự trợ giúp của máy tính, toán học? Trước tiên cần cung cấp cách chứng minh! Tuy nhiên, các nhà<br /> đều chỉ là chân lý tương đối! Điều cho máy tính các kiến thức toán học. toán học sẽ biết cách tìm chỗ đứng<br /> này thực ra không dễ chấp nhận đối Dự án FAB nhằm viết lại dần dần các không thể thay thế được của mình<br /> với nhiều nhà toán học truyền thống. định lý toán học dưới ngôn ngữ hình trong cơn bão 4.0, với những máy<br /> thức để máy có thể “hiểu” được. Khi tính biết tư duy!<br /> Một số nhà toán học còn cực đoan<br /> đã có đủ nhiều kiến thức, với khả Voevodsky (1966-2017), nhà toán<br /> đến mức cho rằng, nếu một chân lý<br /> năng xử lý tín hiệu lớn, máy tính sẽ có học Nga được giải thưởng Fields năm<br /> toán học được chứng minh mà không<br /> lợi thế hơn rất nhiều so với con người 2002, đã đề ra một chương trình lớn<br /> cần đến sự trợ giúp của máy tính thì<br /> trong việc phát hiện ra quy luật, tức được gọi là “Univalent Foundations<br /> đó chỉ có thể là… chân lý tầm thường!<br /> là đưa ra các giả thuyết, đồng thời tìm of Mathematics”, với tham vọng<br /> Họ cho rằng chỉ sau 20, 30 năm nữa<br /> kiếm rất nhanh con đường đi từ giả xây dựng lại toàn bộ cơ sở toán học<br /> thôi, tất cả những gì mà toán học<br /> thiết đến kết luận. theo ngôn ngữ hình thức. Khác với<br /> ngày nay làm được sẽ trở thành quá<br /> dễ với máy tính! Với những nhà toán Ví dụ của chứng minh “1+1=2” đã công việc của Bourbaki, dự án của<br /> học theo quan điểm đó, toán học nêu trên đây phần nào cho ta thấy Voevodsky khi hoàn thành sẽ giúp<br /> cuối cùng sẽ có số phận như môn cờ khó khăn của công việc mà FAB phải kiểm tra tự động các chứng minh toán<br /> vua, khi mà nhà vô địch thế giới có làm: để đưa được mỗi một định lý học. Theo ông, đến ngày đó, khi nhà<br /> thể bị đánh bại dễ dàng bởi một máy thành ngôn ngữ hình thức, cần phải toán học gửi một công trình mới đến<br /> đánh cờ! hình thức hoá rất nhiều khái niệm toà soạn, anh ta sẽ phải gửi thêm một<br /> toán học. chương trình kiểm tra tự động. Như<br /> Dự án FAB vậy, người phản biện không cần kiểm<br /> Dự án FAB được bắt đầu từ năm<br /> FAB (Formal Abstracts in tra tính đúng đắn của bài báo nữa,<br /> 2018, với sự hợp tác của các nhóm<br /> Mathematics) là dự án có một tham mà chỉ nhận xét về tầm quan trọng<br /> nghiên cứu thuộc ba trường đại học<br /> vọng lớn: làm cho máy tính không mà thôi. Tiếc rằng Voevodsky đã ra<br /> là University of Pittsburgh, Carnerie<br /> những có thể kiểm tra tính đúng đắn đi quá sớm, khi dự án đầy tham vọng<br /> Mellon University (Hoa Kỳ) và Trường<br /> của các chứng minh, mà còn phát của ông vẫn còn dang dở ?<br /> Đại học Thăng Long (Việt Nam). Dự<br /> hiện ra các định lý mới, chứng minh án được tài trợ bởi Sloan Foundation, TÀI LIỆU THAM KHẢO<br /> chặt chẽ các định lý đó. Nói cách do giáo sư Thomas Hales, nhà toán<br /> 1. Th. Hales (1994), “The status of<br /> khác, máy tính làm thay công việc học hàng đầu trong lĩnh vực chứng the Kepler Conjecture”, The Mathematical<br /> của nhà toán học. minh hình thức, lãnh đạo. Intelligencer, 16(3), pp.47-58.<br /> Nói cho cùng, công việc của 2. Th. Hales (2005), “A proof of the<br /> Lời kết<br /> nhà toán học là: trên cơ sở quan sát Kepler conjecture”, Annals of Mathematics,<br /> những sự kiện toán học hay những Trong cuốn “Cái bóng của tư 162, pp.1065-1185.<br /> hiện tượng tự nhiên và xã hội, phát duy”, Penrose có nói đại ý: cho đến 3. Th. Hales (2015), Formal proof,<br /> hiện và phỏng đoán một số kết quả nay, bất kỳ một tri thức nào của nhân Notices of the AMS.<br /> có thể có, tức là đặt ra các giả thuyết. loại cũng phải nằm trong một bộ óc 4. V. Voevodsky (2014), Computer<br /> Bước tiếp theo là chứng minh hoặc cụ thể nào đó (nói nôm na, nếu “nhân Proof Assistants and Univalent Foundations<br /> bác bỏ giả thuyết đã đặt ra. Để làm loại” biết điều gì đó thì có nghĩa là ít of Mathematics, CMA 2014.<br /> việc này, nhiều khi phải xây dựng nhất một người biết điều đó!). Mà bộ 5. R. Penrose (1989), Shadows of the<br /> những khái niệm và lý thuyết mới. óc của mỗi cá nhân đều có giới hạn Mind: A Search for the Missing Science of<br /> Một chứng minh chính là một chuỗi của nó. Như vậy, nếu nhân loại có Consciousness, Oxford University Press.<br /> <br /> <br /> <br /> 7<br /> Soá 4 naêm 2019<br />