Mathematics as one should see it ..

 

   

    From stacking oranges to putting the world into forms!

TL;DR: Rất rất dài, nhiều chữ ít hình, cho những ai thích Toán, Tin, truyện cổ tích, cả 3. Hoặc thích nghe tôi kể chuyện.

Có một bài toán nổi tiếng trong lịch sử toán học: Bài toán giả thuyết Kepler.

Đây cũng là bài toán nhiều người bán hoa quả quan tâm:

Xếp các quả cam cách nào tốn ít chỗ nhất?

Vào thế kỷ 17, nhà toán học và thiên văn học người Đức Johanne Kepler phát biểu “Xếp theo hình kim tự tháp là tốt nhất” nhưng ông lại không thể chứng minh. Người ta do đó gọi đây là giả thuyết Kepler.

 Từ lúc phát biểu đến hơn 300 năm sau, giả thuyết này được bàn luận rộng rãi và trở thành 1 trong 23 vấn đề nổi tiếng của toán học. Chưa nhà toán học nào chứng minh được nó đúng, lẫn chưa ai khẳng định được nó sai.

Cho đến 1998, có một người tuyên bố chứng minh được giả thuyết ấy: Thomas Callister Hales – giáo sư Toán của trường đại học Michigan.

Ở Vn, nhờ giáo sư Ngô Bảo Châu, nhiều người lần đầu đã nghe nói đến giải thưởng Fields. Fields là giải lớn nhất trong toán học, tương đương giải Nobel trong các lĩnh vực khác. Nhưng khác Nobel, Fields giới hạn độ tuổi và chỉ dành cho các nhà toán học dưới 40.

Năm 1998, Hales đúng 40 tuổi.

Nếu chứng minh của Hales đúng, khả năng lớn cũng giúp ông đạt huân chương Field.

Chỉ một vấn đề ngăn Hales với giải thưởng nhà toán học nào cũng khao khát này:

Chứng minh giả thuyết Kepler dài 120 trang cùng 3 gigabytes phần mềm tính toán. Đã cần 20 nhà phản biện và 4 năm để kiểm tra chứng minh ấy, và kết luận:

Không thể kiểm tra chứng minh này.

Các phản biện viên có thể chắc chắn về 99% chứng minh, nhưng lại không kiểm tra hết được dữ liệu tính toán.

Có thể tưởng tượng phần nào sự thất vọng của Hales trong tình huống ấy. Song nghịch cảnh cũng là cơ hội vươn lên. Năm 2003, Hales và nhóm nghiên cứu triển khai dự án Flyspeck, mục tiêu là kiểm tra chứng minh kiểu hình thức aka dùng máy tính để kiểm tra chứng minh ông đưa ra. Năm 2014, 16 năm sau khi đưa ra phát biểu gây xôn xao khoa học, Hale hoàn thành Flyspeck, và khẳng định chứng minh của ông là đúng đắn.

Song Thomas Hales có tầm nhìn rộng hơn kết quả mang tính cá nhân đó. Như chia sẻ khi sang thăm Đại học Thăng Long, Hales nói: Lúc đó, tôi đã quyết định biến đây thành mục tiêu cuộc đời. Máy tính biết tính là bởi con người biết tính. Con người biết kiếm tra chứng minh, máy tính cũng có thể sẽ làm được vậy. Tôi muốn có thể xây dựng các phản biện viên ảo hỗ trợ con người, để những tiền lệ như tôi không xảy ra nữa.

Và dự án Formal Abstracts được lập ra hướng đến hình thức hoá và kiểm tra hình thức các kết quả toán học. Hình thức hoá là chuyển sang dạng ngôn ngữ máy tính hiểu được, và khi máy tính hiểu được thì xử lý được, aka kiểm tra hình thức được.

Song khác Flyspeck sử dụng ngôn ngữ hình thức HOL-Light, với Formal Abstracts, Hales chọn một ngôn ngữ khác: Lean.

Lean được phát hành bởi Microsoft Research vào 2013, là một công cụ chứng minh hình thức còn đang phát triển nhưng hứa hẹn. Khác tên gọi của nó (Lean = gọn ghẽ), Lean đầy tham vọng khi kết nối chứng minh tự động với chứng minh tương tác, lập trình phổ thông lẫn chứng minh định lý, lẫn là siêu ngôn ngữ aka dùng Lean mở rộng được chính Lean. Xây dựng thư viện Lean còn chủ yếu bởi nhóm nghiên cứu của Carnegie Mellon University ở Pittsburgh mà Hales trực tiếp liên hệ aka Hales nhận hỗ trợ từ những người sinh ra Lean.

Chỉ một vấn đề nhỏ.

Tức là cũng không nhỏ:

Lean rất khó để thành thạo.

Theo Hales, nếu không đang là sinh viên Stanford hay Carnegie Mellon University định viết khoá luận về Lean, hoặc sinh viên Imperial College London được hướng dẫn bởi Kevin Buzzard (thêm về bác này sau) thì dùng Lean sẽ không thích hợp.

Nhưng rõ ràng, dự án của Hales cần nhiều hơn một đội ngũ các chuyên gia, và chỉ thành công khi thu hút một cộng đồng những nhà toán học cùng đóng góp. Vậy nên làm thế nào?

Hales nghĩ tới một cầu nối giữa ngôn ngữ toán học tự nhiên và ngôn ngữ hình thức, hay như cách ông dùng “some kind of gateway drugs to Lean”.

Dự án kết nối CNL và Lean ra đời, với CNL là viết tắt cho Controlled Natural Language – ngôn ngữ tự nhiên có kiểm soát - cầu nối mà Hales muốn xây dựng.

Thực ra, không phải chỉ đến bây giờ người ta mới nghĩ tới ý tưởng tương tự. Năm 1970, Victor Krushskov - nhà Toán học Xô Viết cha đẻ của ngành công nghệ thông tin lẫn tiên phong trong ngành điều khiển học của nước Nga, cũng đã đề xuất ý tưởng kết hợp ngôn ngữ tự nhiên và hình thức, khi ấy phục vụ một chương trình chứng minh tự động của Nga tên là Evidence Algorithm.

Tại sao một nhà toán học chọn phân rã chuỗi chứng minh của ông ta thành một lược đồ bao gồm các bổ đề đặt chính xác ở các mốc này mà không phải ở mốc kia? Điều ấy không luôn là một sắp xếp ngẫu nhiên, cũng không phải một quy luật tổng quát, mà phản ánh linh tính cá nhân nào đó về cách mỗi người giải quyết vấn đề trong thế giới thực. Nhưng ngôn ngữ hình thức bất lực trong mô tả những sự thật kiểu ấy, các chủ ý mang tính biểu tượng sẽ biến mất hoàn toàn trong chuỗi logic sinh từ máy tính. Một ngôn ngữ kết hợp giữa hình thức và tự nhiên có thể lưu giữ các thông tin không tường minh song có ích như thế.

Ý tưởng này nằm trong hiếm hoi những điều Tây Âu và Đông Âu đồng ý bất chấp Chiến tranh lạnh. Các phiên bản ngôn ngữ lai cho tiếng Anh lần lượt ra đời, trong đó có ForTheL - Formal Theory Language, ngôn ngữ lõi cho bộ chứng minh SAD – System for Automated Deduction.

SAD được đề xuất vào 1980, nhưng 2008 mới được cài đặt trong luận án tốt nghiệp của một nhà toán học trẻ người Uckraine là Andrei Paskevich. Từ bước ngoặt này, vào 2017, SAD lại được mở rộng để kết hợp với ngôn ngữ chứng minh Isabelle, nằm trong dự án Naproche-Isabelle tại đại học Bonn của giáo sư Peter Koepke.

Và Koepke, 2 năm sau, là người Hales sẽ gặp bàn về CNL.

Nếu ForTheL, một ngôn ngữ lai khá giống ngôn ngữ toán học tự nhiên, song chỉ xử lý logic bậc nhất, vẫn có thể là đầu vào cho một ngôn ngữ xử lý logic bậc cao như Isabelle, điều tương tự liệu có thể với ngôn ngữ bậc cao khác là Lean?

Mọi thứ vẫn đang trong nghiên cứu, nhưng kết quả là hứa hẹn.

Hales lại tiếp tục gặp những khó khăn khác.

Tin tốt là chúng không về kỹ thuật.

Và tin xấu là chúng không về kỹ thuật.

Một số ý tưởng khi ra đời sẽ vấp phải sự e ngại từ những người mong mọi chuyện đừng thay đổi.

Với Hales còn cả e ngại từ những người thích thay đổi.

Một mặt, nhiều nhà Toán học tỏ ra nghi ngờ viễn cảnh hình thức hoá các kết quả Toán học hay sự ra đời của một công cụ kiểm tra chứng minh hoàn toàn tự động. Sự e dè này không chỉ là một chất vấn về tính khả thi. Có lúc điều này là một phản ứng thực tiễn, xuất phát từ nỗi sợ hiện sinh rằng liệu người ta có còn cần những nhà toán học. Có cả những lúc nó là một phản ứng có tính lý tưởng, một niềm tin rằng Toán học nên là một trò chơi thuần khiết thông minh cần cả tưởng tượng hy vọng lẫn nỗ lực trong bất định, hơn là một thứ máy móc, công nghiệp, và tất định.

Mặt khác, một số nhà Toán học lại siêu háo hức với Lean và tự hỏi sao phải sinh ra CNL, sao chúng ta không dạy luôn Lean cho bọn trẻ con trong chương trình Toán từ giờ. Đây chính là một số ít người đã kịp học Lean, đã thấy ích lợi thực tiễn với nghề nghiệp của họ, và không hề muốn chờ người đến sau. Có thể họ không nhận ra, kịch bản này hơi giống lần tôi nói về hệ thống ký âm âm nhạc, đó là một ngôn ngữ bị trở thành một công cụ cho elitism, để kiến thức bị phong bế trong một circle và làm nên lợi thế cạnh tranh của họ với phần còn lại xã hội. Theo cách ấy, CNL là một nỗ lực dân chủ hoá Lean.

Nói cách khác, Hales đang đi giữa 2 làn đạn, cả người cho rằng ông đi quá nhanh lẫn những người cho rằng chớ nên chậm lại.

Song chẳng còn con đường nào khác.

Thực ra ở đây, Hales cần trả lời ko chỉ câu hỏi:

Hoặc:

Mà còn cả:

Có hai lý do để tôi chọn tin câu trả lời cho câu cuối trên là "Có", trong ấy một lý do cá nhân và một lý do phổ quát.

Hãy nói về lý do phổ quát trước, và quay về với Kevin Buzzard.

Trong bài thuyết trình mới đây tại CMU, mặc cái quần loè loẹt đặc trưng, với dáng đi vừa chúi về phía trước vừa hấp tấp vung vẩy như một đứa trẻ cả tự kỷ lẫn tăng động, Buzzard đã nói về tương lai của Toán học.

Ông kể về một ngày nọ năm ngoái khi ông "gặp một tay ở Google tên là Christian Szegedy", kẻ mà “tôi chẳng chắc là thiên tài hay điên nữa”, kẻ đang xây dựng dự án chứng minh tự động mà một tay nữa từ Google Research còn mới khoe khoang ở CMU cách đây mấy hôm, cũng là kẻ khẳng định “trong 10 năm nữa, máy tính sẽ làm Toán tốt hơn con người” – và nhà toán học người Anh này kết luận “không nghi ngờ gì nữa, thằng cha này bị điên”.

Song chẳng gì kịch tính hơn “nhưng mà” và là một fan hiển nhiên của kịch tính, Buzzard tự hỏi:

Nhưng mà lỡ gã điên này lại đúng?

"Đầu tiên thì, thế nào là một chứng minh Toán học" - Buzzard đặt câu hỏi.

Một người mới làm Toán và một chương trình máy tính, đều sẽ cho trả lời giống nhau:

"Là một chuỗi suy luận dựa trên các tiền đề được công nhận và các kết quả được chứng minh khác, để dẫn ra một kết quả."

Nhưng với người làm Toán chuyên nghiệp, mọi thứ không còn lý tưởng như thế:

Theo Buzzard, chứng minh có lúc chỉ là thứ được chấp nhận bởi “các bô lão" aka tạp chí uy tín hàng đầu như Annals of Mathematics. Và thật sự uy tín như Annals of Mathematics, thì vẫn có lúc xuất bản những kết quả trái ngược nhau - aka ít nhất một bị sai - mà không hề đính chính.

Buzzard liệt kê tiếp các “vật chứng” về các lỗ hổng Toán học bị lờ đi, như thể tồn tại những open secrets ngầm hiểu giữa các chuyên gia Toán lâu năm và che đi với người bắt đầu làm Toán.

Ông tự hỏi: Liệu chúng ta có cần thuộc về nhóm chuyên gia trên để biết điều gì nên tin trong Toán? Nếu Toán học không thể kiểm nghiệm khách quan, nó còn là khoa học?

Buzzard nhắc đến một kết quả ông từng xuất bản. Ông nói: Tôi tin với xác suất 99.9% là kết quả này sẽ chẳng bao giờ được con người dùng trong bất kỳ mục đích nào hữu ích. Điều duy nhất khiến tôi theo đuổi nó là vẻ đẹp của sự thật. Nhưng nếu giờ niềm tin đó cũng lung lay, chẳng phải toàn bộ việc ấy là vô ích hay sao?

Đến đây Buzzard thú nhận:

Gã Szegegy ấy, có lẽ còn chưa điên.

Bởi vì:

Cũng nghĩa là, nếu người ta muốn Toán học đúng như những gì được định nghĩa với xã hội, aka muốn Toán học đúng là Toán học, thì sử dụng máy tính để kiểm tra chứng minh không chỉ là giải pháp, có thể là một tất yếu.

Và giờ tôi sẽ nói về lý do cá nhân.

Một truyện cổ tích tôi rất thích là Blue Beard. Mẹ đọc truyện này hồi tôi bé ở Nga, từ một tập truyện cổ tích mỏng có đầy tranh bằng tiếng Nga. Mẹ dịch là Ông Râu Xanh thay vì Con Yêu Râu Xanh, nên lúc đó nghe tôi chẳng hề thấy sợ hãi, chỉ cảm thấy câu truyện ấy thật kỳ lạ. Khi tôi lớn hơn, càng nhận thấy Blue Beard là một dụ ngôn thú vị. 

Lược đồ của Blue Beard cũng là một bí mật, cùng một yêu cầu phải phong bế bí mật ấy, một kiểu tình tiết mà ai hay đọc cổ tích đều biết là đang gào lên: Đừng mở ra, dừng lại ngay đi, trước khi gặp thảm hoạ.

Cùng lúc, ai hay đọc cổ tích cũng đều biết rằng: hẳn nhiên sẽ không thể dừng lại; rằng giây phút cánh cửa cuối cùng kia mở ra, trong cảnh tượng bao xác phụ nữ không đầu chất chồng lên nhau vấy máu, hơi gió tanh tưởi sẽ thì thầm: quá muộn rồi, giờ thì đến lượt mày.

Nhưng tất nhiên, cô gái cuối cùng sẽ được cứu, ông râu xanh cuối cùng sẽ bị giết, và cả làng cuối cùng sẽ không còn những phụ nữ mất tích.

Nói cách khác, thông điệp của Blue Beard là:

Khai mở bí mật chắc chắn sinh ra thảm hoạ. Tuy nhiên, vẫn nhất định phải khai mở. Và thảm hoạ rồi thì cũng sẽ được giải quyết.

Tinh thần nỗ lực mở tung bí mật ấy, như cái ấn tượng của một ngọn hải đăng chiếu một tia sáng không khoan nhượng đâm xuyên vào vào bóng tối, chính là đặc trưng của tính nam lẫn văn minh phương Tây, một thứ khao khát muốn ép cái bất định đi vào khuôn khổ, nặn cái hỗn độn thành hình hài, và khiến những thứ mập mờ phải lồng lộng hiển ngôn. Theo Plato, bố già không chính thức của nền văn minh 2 thiên niên kỷ này, đó có lẽ chính là create order from chaos and put things into forms. Tôi tin thuyết cho rằng Thiên Chúa Giáo có mượn cảm hứng từ Neoplatonism, và với tôi, Chúa rất giống một phiên bản nhân cách hoá và huyền học hoá cho khái niệm Form của Plato, thứ hiện hữu trong vạn vật, song không phải là bất cứ cái gì trong vạn vật.

Nhưng Bertrand Russell đã nhận định rất đúng rằng, kể cả thiên hướng trên cũng sẽ chỉ là vấn đề của sở thích. Không phải ai cũng thích sự sáng rõ. Một số người thích truy ngược về cảm giác mơ hồ của một đứa trẻ lẫn một con khỉ, và cho rằng kinh nghiệm nguyên thuỷ là con đường đến với sự thông thái tốt hơn so với kinh nghiệm của sự khai phá. Song có thể giống Russell, dường như Hales và Buzzard đều thích ngược lại.

Đến đây quay về với tầm nhìn của Formal Abstract. Có thể, thử nghiệm hình thức hoá là một nỗ lực nếu thành công cũng phá đi cái tự nhiên nguyên thuỷ nào đó của Toán học, một sự liều lĩnh mở toang cánh cửa cuối cùng mà không biết đang tiến rất gần thảm hoạ, ít nhất như Buzzard dự đoán “rồi chính nhờ công cụ này, tụi trẻ con làm Toán sẽ bắt đầu chất vấn người lớn chúng ta những câu hỏi chẳng dễ dàng”.

Nhưng rồi, vẫn sẽ có những người hăng hái chọn con đường ấy, dẫu cho có thể vấy máu hay tanh tưởi. Và sau rốt, nếu thảm hoạ xuất hiện, họ sẽ chấp nhận giải quyết chúng với cùng sự hăng hái tương đương.

Không gì minh hoạ thái độ này cô đọng bằng câu Hales trích sau của Nick Horton:

Nói chung, không cách nào kết thúc một bài viết kỹ thuật hợp lý bằng hót lên một khúc vĩ thanh mang màu sắc giai thoại danh nhân mà đời thường gần gũi.

Và khúc vĩ thanh tôi sắp hót đây được bắt đầu ngay ngày chúng tôi đến Pittsburg. Hales nói mai dẫn team đi chơi tubing, một trò chơi mà mỗi người ngồi trên một cái phao hình tròn và trượt từ núi tuyết xuống.

Tôi hỏi “Tubing cần kỹ thuật gì không?”

Hales đáp “Không gì ngoài dũng cảm.”

Tôi nói với mọi người “Thế chỉ cần liều thôi”, nghĩ bụng:

Dân Việt Nam đây liều mà thứ hai thì đố ai dám thứ nhất!

Nhưng đến khi tubing mới biết, hoá ra dân Việt Nam đây chưa liều như tôi tưởng.

Khi trượt xuống, dù căn chỉnh thì phao vẫn xoay và bạn không thể nhìn được sẽ đi về đâu. Không điểm tựa và lao xuống từ đằng lưng, người ta dễ cảm giác như phao sắp đâm vào hàng rào bên núi, hay là gọn ghẽ hơn, mình sẽ bắn văng ra và cắm đầu một cách đầy trừu tượng trong tuyết.

Kết cục, khi trượt tôi rú rít tim tý nữa bay ra đằng miệng và sự liều lẫn lòng dũng cảm nếu tồn tại hẳn đều đọng thành vũng dưới chân.

Nhưng sau vài lần chơi thì, sự sợ hãi bắt đầu giảm và thay bằng niềm phấn khích. Tôi bắt đầu muốn trượt nữa, trượt nữa, trượt đôi, trượt đơn, rồi đua trượt. Trong nhóm có chị N còn máu hơn. Chị tính trượt cả kiểu nằm sấp, khó hơn và trông hãi hơn, và cuối cùng làm được thật. Có vẻ chỉ cần sắp tư thế y như Hales hướng dẫn, rồi giữ vậy cho chắc thì không thể văng được aka chỉ cần đúng kỹ thuật.

Chơi chán tubing xong, chúng tôi đi về ra xe. Ngang qua một bãi tuyết cao, Hales ngã xuống, tay đập đập. Cảnh này cute vãi nên chúng tôi làm thử luôn. Tôi nói Hales là mọi người bảo chúng ta trông như vịt đang vẫy cánh, ông nói: Không, không phải vịt đâu, là angel đấy.

Đến đoạn này thì đã sắp xong một thiên anh hùng ca trượt tuyết, nhưng đáng ra tôi nên viết về giai thoại danh nhân cơ mà nhỉ? Danh nhân đâu? Và giai thoại chỗ nào?

Tất nhiên, mọi anh hùng ca vĩ đại đều không thể thiếu một điểm rơi, một cú twist and turn nào đó. Và twist and turn của câu chuyện tubing trên chính là:

Hales hoá ra mới tubing lần đầu.

Thế mà thanh niên này chém về kinh nghiệm kỹ thuật này nọ y như thật. Mà nghe theo mớ chặt chém hùng hồn của ông, N không những dám trượt, lại còn trượt thành công.

Như thế thì không hẳn kỹ thuật, có thể chính niềm tin chị đang chơi đúng đã thực sự giúp N chơi đúng. Aka, again, chẳng cần gì ngoài một chút liều lĩnh.

Nhưng không chỉ tubing, nhiều thứ trong đời cũng như vậy.

Dự án của Hales nữa, cũng có lẽ sẽ cần đến một niềm tin như thế, một nguồn sáng đủ lớn, chiếu thẳng, và không khoan nhượng ..