Exploring the Educational Value of Mathematical Beauty and Effective Ways of Discovering Mathematical Beauty

The precision of mathematical reasoning, the abstractness of mathematical language, the profundity of mathematical thought and method, as well as the excessive formalization of mathematics teaching have formed an impassable gap, hindering students in approaching mathematics. This has concealed the beauty of mathematics and the light of mathematical culture. However, if students are able to cross this gap, they would find that mathematics is a vast world full of vitality, imagination, wisdom, poetry, and beauty. The pursuit of mathematical beauty is one of the motivations for scientists to research this field. Experiencing mathematical beauty is of great significance to students’ learning and growth. In teaching, the value of mathematical beauty is explored, such as stimulating emotions, opening up to the truth, and cultivating goodness. Several effective ways are suggested in this article to guide students to discover the mathematical beauty in life while finding it in problem-solving methods and exploring it in knowledge systems.

Formalization of the Equivalence among Completeness Theorems of Real Number in Coq

The formalization of mathematics based on theorem prover becomes increasingly important in mathematics and computer science, and, particularly, formalizing fundamental mathematical theories becomes especially essential. In this paper, we describe the formalization in Coq of eight very representative completeness theorems of real numbers. These theorems include the Dedekind fundamental theorem, Supremum theorem, Monotone convergence theorem, Nested interval theorem, Finite cover theorem, Accumulation point theorem, Sequential compactness theorem, and Cauchy completeness theorem. We formalize the real number theory strictly following Landau’s Foundations of Analysis where the Dedekind fundamental theorem can be proved. We extend this system and complete the related notions and properties for finiteness and sequence. We prove these theorems in turn from Dedekind fundamental theorem, and finally prove the Dedekind fundamental theorem by the Cauchy completeness theorem. The full details of formal proof are checked by the proof assistant Coq, which embodies the characteristics of reliability and interactivity. This work can lay the foundation for many applications, especially in calculus and topology.

Formalization of mathematics through proof assistants

The formalization of mathematics in practice relies heavily on proof assistants and automatic theorem provers, therefore we studied what are the state of the art proof assitants and their limitations to understand what are the main challenges in making formalized mathematics common practice among mathematicians. We found out that curretly the two major dificulties in formalizing mathematics with proof assistants are due to steep learning curves in how to use these tools and due to a wide gap between the notation employed in these proof assistants and the currently used mathematical notation. We also developed a C++ library to develop proof assistants with great notational flexibility.

An experimental library of formalized Mathematics based on the univalent foundations

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).