Formalized mathematics represents a revolution in mathematics. Combining theorem provers for 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. Notably, in May 2025, the internationally renowned mathematician Terence Tao initiated a project based on the Lean theorem prover to implement the formalization of mathematical analysis, generating significant impact across both the mathematical and computer science communities. This paper 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 currently 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. Our system is strictly corresponded to the textbook content, where all theorems are provided with machine-verifiable Coq proof. The entire formalization has been 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.