Toán học thời 4.0 và dự án 'Formal Abstract in Mathematics' (FAB)

Trong bài viết này, tác giả đề cập về vai trò của máy tính trong nghiên cứu Toán học dưới tác động của cách mạng công nghiệp lần thứ 4, và giới thiệu về dự án FAB “Formal Abstract in Mathematics”, một dự án mà Trường Đại học Thăng Long đã tham gia thực hiện cùng với hai trường đại học lớn của Mỹ là University of Pittsburgh và Carnegie Mellon University
Nội dung trích xuất từ tài liệu:
Toán học thời 4.0 và dự án “Formal Abstract in Mathematics” (FAB) Tạp chí Khoa học Đại học Thăng Long A1(1):144-164, (2021) THÔNG TIN - DIỄN ĐÀN TOÁN HỌC THỜI 4.0 VÀ DỰ ÁN “FORMAL ABSTRACT IN MATHEMATICS” (FAB) Hà Huy Khoái*, Nguyễn Thị Huyền Châu**, Nguyễn Thị Trà My**, Mai Thúy Nga***, Ngô Thị Thanh Nga**** © 2021 Trường Đại học Thăng Long. Nhận bài: 20/07/2021; Chấp nhận đăng: 10/08/2021 Trong bài báo này chúng tôi đề cập về vai trò của máy tính trong nghiên cứu Toán học dưới tác động Tóm tắt của cách mạng công nghiệp lần thứ 4, và giới thiệu về dự án FAB “Formal Abstract in Mathematics”, một dự án mà Trường Đại học Thăng Long đã tham gia thực hiện cùng với hai trường đại học lớn của Mỹ là University of Pittsburgh và Carnegie Mellon University. Chúng tôi cũng giới thiệu những nét căn bản về hệ chứng minh hình thức Lean (ngôn ngữ được dùng để viết hình thức hóa các định lý trong 100 định lý phổ biến của toán học, ở giai đoạn đầu của dự án) và CNL (Controlled Natural Language, sử dụng ở giai đoạn sau của dự án). Từ khóa: Trừu xuất hình thức; Chứng minh hình thức; Ngôn ngữ tự nhiên có kiểm soát, Colada, Lean, mạnh do con người tạo ra). Ngay với những lĩnh vực tư duy có tính cá thể cao như Toán học, máy 1. Toán học thời 4.0 và dự án FAB Người ta thường nhắc câu nói nổi tiếng của tính đang mang đến những thay đổi khó hình 1.1. Archimede với đòn bẩy Archimede: “Hãy cho tôi một điểm tựa, tôi sẽ nâng dung. “Nghề làm Toán trong thời đại 4.0” có thể được cả Trái đất!” Nói cách khác, với Archimede sẽ rất khác với những gì vẫn được hiểu hàng ngàn thì cái đòn bẩy tạo sự bình đẳng về sức lực cơ bắp năm nay. Cuộc cách mạng công nghiệp lần thứ 4 giữa người yếu và người khoẻ. không chỉ tạo ra làn gió mới, mà thậm chí là cơn bão trong Toán học, và kéo theo nó, không những Vậy thì cái gì có thể xem là đòn bẩy cho “sức là hứng khởi, hân hoan, mà cả sự nghi ngờ, tranh lực” của trí tuệ? Không gì khác hơn là máy tính cãi nữa. (tất nhiên với những chương trình ngày càng * Viện Toán học và Khoa học ứng dụng Thăng Long (TIMAS), Trường Đại học Thăng Long ** Phòng thí nghiệm Trí tuệ nhân tạo, Trường Đại học Thăng Long *** Bộ môn Tin, Khoa Toán - Tin, Trường Đại học Thăng Long **** Bộ môn Toán, Khoa Toán - Tin, Trường Đại học Thăng Long 144 Hà Huy Khoái, Nguyễn Thị Huyền Châu, Nguyễn Thị Trà My, Mai Thúy Nga, ... Những vấn đề cốt lõi lại một lần nữa được đặt mà trong công việc của thầy giáo Toán, một phần ra: thế nào là “chân lý Toán học”, thế nào là một lớn là làm cho học sinh hiểu được những lập luận “chứng minh”? Phần viết này nhằm giới thiệu logic trung gian đã bị bỏ qua trong chứng minh. với bạn đọc một số vấn đề xuất hiện khi sử dụng Mặt khác, các yếu tố trực giác thường được máy tính trong chứng minh Toán học, và hơn nữa, sử dụng, nhất là trong các chứng minh hình học, trong việc thay thế dần lao động của nhà Toán 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 Vào thế kỉ VI và VII trước Công nguyên, các ngắn gọn trình bày chứng minh, và tất nhiên khi 1.2. Chứng minh Toán học học giả Hy Lạp đã đưa ra cái mà về sau gọi là suy cần, họ phải có lập luận logic chặt chẽ mà không luận logic: đó là chuỗi các suy luận – các phép viện đến trực giác. tam đoạn luận – chúng buộc người đối thoại chấp Với việc bỏ qua một số lập luận logic và sự nhận khẳng định Q một khi đã đồng ý một khẳng tham gia của trực giác, vấn đề đặt ra là: các định định P trước đó. Ta biết rằng, từ thế kỷ thứ V lý Toán học có đáng tin cậy hay không? Chúng ta trước công nguyên, các nhà tư tưởng Hy Lạp đã thường tin và sử dụng trong công việc của mình là những bậc thầy về nghệ thuật sắp xếp lý luận những định lý mới, những kết quả mới của Toán thành một chuỗi liên tiếp các kết luận logic, điều học, nếu đó là kết quả của nhà Toán học “có uy này được thấy rõ trong các tác phẩm của những tín”, và đăng tải trên những tạp chí “đáng tin cậy”. nhà ngụy biện, cũng như trong các đoạn đối thoại Tuy nhiên, rõ ràng điều này không đảm bảo tuyệt của Plato. Họ khám phá ra rằng, những lý luận đối cho sự đúng đắn của các định lý đó. Nhà Toán này có thể lấy bất cứ hoạt động nào của con người học nào cũng có thể sai lầm khi bỏ qua các lập làm đối tượng, đặc biệt là những công thức toán luận logic trung gian, và người duyệt đăng cũng học và hình học, hầu hết trong số đó đến từ nền vậy. Trong bài này, chúng tôi cũng sẽ đưa ra một văn minh Ai Cập và Babylon. Những lý luận này số ví dụ về sai lầm của các nhà Toán học. trở thành chứng minh kết nối những định lý với Với những định lý mà chứng minh tương đối nhau. Những chứng minh đầu tiên được tìm thấy ngắn, người ta có thể kiểm tra từng dòng chứng trong Analytica Posteriora của Aristotle, theo đó, minh để bảo đảm những lập luận trung gian đã bị các định lý được suy ra từ một chuỗi lập luận bỏ qua thực sự là đúng đắn. Tuy nhiên điều này mà người đọc hiểu được không cần giải thích gì không dễ khi chứng minh dài khoảng 100 trang, thêm, và một số tiên đề được chấp nhận. hay hơn nữa. Đặc biệt, với những chứng minh có Chứng minh toán học theo hình mẫu của sự trợ giúp của máy tính thì tính đúng đắn của nó Aristotle và Euclid có hai đặc điểm nổi bật là bỏ là điều không dễ chấp nhận. Đặc điểm chung của qua nhiều suy luận logic trung gian và dựa nhiều những chứn ...