The formalization of mathematics has become increasingly popular in recent years. Formalization refers to the expression of mathematical definitions and proofs within a precisely defined system of rules, allowing software programs to verify their correctness. This thesis formalizes Schwartz functions using the interactive theorem prover Lean, which provides automation and feedback during the construction of definitions and arguments. Due to their smoothness and rapid decay at infinity, the space of Schwartz functions forms a natural setting for the Fourier transform. While Lean's library already contains an abstract formalization of Schwartz functions, this thesis presents a more concrete, coordinate-based approach that aligns more closely with standard mathematical textbooks. The knowledge gained throughout this thesis can support future formalizations of results in distribution theory, a domain that is still underdeveloped in Lean.