The Machine-Checked Complete Formalization of Landau’s Foundations of Analysis in Rocq

Formal verification has achieved remarkable outcomes in both theory advancement and engineering practice, with the formalization of mathematical theories serving as its foundational cornerstone—making this process particularly critical. Axiomatic set theory underpins modern mathematics, providing the rigorous basis for constructing almost all theories. Landau’s Foundations of Analysis starts with pure logical axioms from set theory, does not rely on geometric intuition, strictly constructs number systems, and is a benchmark for axiomatic analysis in modern mathematics. In this paper, we first develop a machine proof system for axiomatic set theory rooted in the Morse–Kelley(MK) system. This system encompasses effective proof automation, scale simplification, and specialized handling of the classification axiom for ordered pairs. We then prove the Transfinite Recursion Theorem, leveraging it to further prove the Recursion Theorem for natural numbers—the key result for defining natural number operations. Finally, we detail the implementation of a machine proof system for analysis, which adopts MK as its description language and adheres to Landau’s Foundations of Analysis. This formalization realized all the contents of the book from natural numbers to complex numbers. All formalization does not need to introduce the standard library and has undergone verification by Rocq(Coq) 8.16 to ensure reliability. Implemented using the Rocq proof assistant, the formalization has undergone verification to ensure reliability. This work holds broader applicability such as the formalization of point-set topology and abstract algebra, while also serving as a valuable resource for teaching axiomatic set theory and mathematical analysis.