## Summary

We formalize in the Mizar system [3], [4] basic definitions of commutative ring theory such as prime spectrum, nilradical, Jacobson radical, local ring, and semi-local ring [5], [6], then formalize proofs of some related theorems along with the first chapter of [1].

The article introduces the so-called Zariski topology. The set of all prime ideals of a commutative ring *A* is called the prime spectrum of *A* denoted by Spectrum *A*. A new functor Spec generates Zariski topology to make Spectrum *A* a topological space. A different role is given to Spec as a map from a ring morphism of commutative rings to that of topological spaces by the following manner: for a ring homomorphism *h* : *A* → *B*, we defined (Spec *h*) : Spec *B* → Spec *A* by (Spec *h*)(𝔭) = *h*
^{−1}(𝔭) where 𝔭 *2* Spec *B*.