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