Article Sidebar

PDF
Date Published: 30/11/2021
Online Published: 21/02/2023
Abstract Views: 139
Views PDF: 86
Issue
No. 1 (2021)
Section
INFORMATION - FORUM
How to Cite
Ha, H. K., Nguyen, T. H. C., Nguyen, T. T. M., Mai , T. N., & Ngo, T. T. N. (2023). MATHEMATICS IN THE ERA OF INDUSTRY 4.0 AND “FORMAL ABSTRACT IN MATHEMATICS” (FAB) PROJECT. Thang Long Journal of Science: Applied Science, 1, 144 - 164. https://science.thanglong.edu.vn/index.php/vola/article/view/20

MATHEMATICS IN THE ERA OF INDUSTRY 4.0 AND “FORMAL ABSTRACT IN MATHEMATICS” (FAB) PROJECT

Huy Khoái Ha, Thi Huyen Chau Nguyen, Thi Tra My Nguyen, Thuy Nga Mai , Thi Thanh Nga Ngo

Main Article Content

Abstract

This paper firstly discusses the use of computer technology for aiding mathematics research in the era of Industry 4.0, the prospect of which has provided the drive behind “Formal Abstracts in Mathematics” (FAB) project, a collaborative work between Carnegie Mellon University, University of Pittsburgh, and Thang Long University. Then, the paper presents an overview of Lean, a theorem prover that was used in the first stage of FAB and is based on the calculus of constructions with inductive types (CiC). Employing this powerful interactive system, FAB has succeeded in formalizing a large part of the 100 most popular theorems list. In the second phase, FAB has turned to the study of CNLs (Controlled Natural Language) and on how to devise such a tool for bridging the gap between the language of Lean and that of the mathematical community.

Article Details

Keywords

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

References

[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/