Thanh bên bài viết

PDF
Ngày xuất bản: 30/11/2021
Ngày xuất bản Online: 21/02/2023
Số lượt xem tóm tắt: 133
Số lượt xem PDF: 85
Số xuất bản
Số 1 (2021)
Chuyên mục
THÔNG TIN - DIỄN ĐÀN
Trích dẫn bài báo
Hà, H. K., Nguyễn , T. H. C., Nguyễn , T. T. M., Mai , T. N., & Ngô, T. T. N. (2023). TOÁN HỌC THỜI 4.0 VÀ DỰ ÁN “FORMAL ABSTRACT IN MATHEMATICS” (FAB). Tạp chí Khoa học Thăng Long: Khoa học Ứng dụng, 1, 144 - 164. https://science.thanglong.edu.vn/index.php/vola/article/view/20

TOÁN HỌC THỜI 4.0 VÀ DỰ ÁN “FORMAL ABSTRACT IN MATHEMATICS” (FAB)

Hà Huy Khoái1, Nguyễn Thị Huyền Châu2, Nguyễn Thị Trà My2, Mai Thúy Nga3, Ngô Thị Thanh Nga4,
1 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
2 Phòng thí nghiệm Trí tuệ nhân tạo, Trường Đại học Thăng Long
3 Bộ môn Tin, Khoa Toán - Tin, Trường Đại học Thăng Long
4 Bộ môn Toán, Khoa Toán - Tin, Trường Đại học Thăng Long

Nội dung chính của bài viết

Tóm tắt

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 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).

Chi tiết bài viết

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

Tài liệu tham khảo

[1] Asperti A., Ricciotti W., Sacerdoti Coen C., and Tassi E., (2011), The Matita Interactive Theorem Prover, in Automated Deduction – CADE-23, vol. 6803, pp. 64–69.
[2] Bansal, K., Loos, S., Rabe, M., Szegedy, C., and Wilcox, S. (2019), HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving, in International Conference on Machine Learning, May 2019, pp. 454–463.
[3] Doorn, F.V., Ebner, G., and Lewis, R. Y., (2020), Maintaining a Library of Formal Mathematics, ArXiv200403673 Cs Math, vol. 12236, 2020, pp. 251–267.
[4] Hales, T., (1994), The status of the Kepler Conjecture, The Mathematical Intelligencer 16 (3), 47-58.
[5] Hales, T., (2005), A proof of the Kepler conjecture, Annals of Mathematics, 162 (2005), 1065–1185
[6] Hales, T., (2015), Formal proof, Notices of the AMS, N.11.
[7] Hales, T., (2019), An argument for controlled natural languages in mathematics, June 4.
[8] Hales, T., (2019), Reader’s guide to the Colada Language.
[9] Hales, T., (2020), Controlled natural language for type theory, AITP 2020.
[10] Hales, T., (2020), Formal Methods in Mathematics, Conference of Lean Together 2020.
[11] Hales, T., (2019), Guidelines for the Planet-Math translation to Colada.
[12] Knuth, D. E., (July 1965), On the translation of languages from left to right (PDF), Information and Control, 8 (6): 607–639. DOI:10.1016/ S0019-9958(65)90426-2.
[13] Moura, L.D., Kong, S., Avigad, J., Doorn, F.V, and Raumer, J.V, (1995), The Lean Theorem Prover (System Description), in Automated Deduction - CADE-25, vol. 9195, pp. 378–388.
[14] Nipkow, T., Paulson, L. C., and Wenzel, M., (2002), Isabelle/HOL: A Proof Assistant for Higher- Order Logic, Springer Science & Business Media.
[15] Penrose, R., (1989), Shadows of the Mind: A Search for the Missing Science of Consciousness, Oxford University Press.
[16] Voevodsky, V., (2014), Computer Proof Assistants and Univalent Foundations of Mathematics CMA 2014, Kuwait.
[17] The Coq Proof Assistant, https://coq.inria.fr/
[18] The Lean Prover Mathlib, https://github.com/ leanprover-community/mathlib
[19] The Top 100 Theorems, http://pirate.shu.edu/~kahlnath/Top100.html
[20] PlanetMath, https://planetmath.org/