Formalized mathematics represents a revolution in mathematics. The combination of theorem provers with machine verification of mathematical theorems establishes not only a new standard for mathematical rigor but also a novel approach to developing mathematics. As mathematical challenges worldwide are increasingly solved with computer assistance and various formalization projects are launched by experts, the influence of formalized mathematics continues to grow. It generated significant impact across both the mathematical and computer science communities. This study introduces a formal system for mathematical analysis based on the Coq theorem prover. The formalization is guided by the textbook Mathematical Analysis compiled by the School of Mathematical Sciences at East China Normal University. Developed within the framework of naive set theory and elementary number theory and algebra, the system has formalized the content related to single-variable calculus from the first volume of the textbook. It includes topics such as real numbers and functions, sequence limits, function limits, continuity of functions, derivatives and differentials, indefinite integrals, and definite integrals. The proposed system strictly corresponds to the textbook content, where all theorems are provided with machine-verifiable Coq proofs. The entire formalization is verified by Coq and executed successfully on a computer. Readers can learn mathematics by following the code and can also understand the code by comparing it with the mathematics, which demonstrates the readability, interactivity, and intelligence of Coq-based machine theorem proving. It represents an attempt to enable readers to follow the computer in learning, understanding, constructing, educating, and even developing modern mathematics, thereby enhancing their ability to understand, experience, and appreciate mathematics.