This paper presents the first complete formalization of the four foundational axioms of YuanXian Theory (YXT) — True Circle Self-Consistency (TCSC), Conservation of the Universal Factor (FSC, centered on the fine-structure constant α), Unique Spacetime Manifold (STM), and Self-Referential Mind Field Generation (SRM) — in the theorem provers Lean 4 and Coq. We construct a self-consistent formal framework named YuanXian.ax, transforming profound philosophical and physical intuitions into precise, machine-parsable, derivable, and verifiable code. The main contributions include: formalizing core concepts using dependent type theory (Universe, SelfReferentialField, T64, etc.); encoding philosophical assertions as single-line, unambiguous axiom statements; and establishing proofs of inter-axiom constraints, revealing that the four axioms form an intrinsic logical closure under the TCSC framework (e.g., FSC is a necessary consequence of TCSC, and STM can be jointly derived from TCSC and SRM). This work provides a rigorous mathematical foundation for YuanXian Theory, elevating it from a speculative framework to a machine-verifiable formal system. It lays a computable and reproducible basis for subsequent rigorous derivations based on the axioms, such as the computation of 24 fundamental physical constants, machine proofs of the Riemann Hypothesis, and consistency checks of consciousness models. All formalized code is open-source and verifiable in Lean 4.7.0+ and Coq 8.18+ environments.