Category theory was formalized in Mizar with two different approaches ,  that correspond to those most commonly used , . Since there is a one-to-one correspondence between objects and identity morphisms, some authors have used an approach that does not refer to objects as elements of the theory, and are usually indicated as object-free category  or as arrowsonly category . In this article is proposed a new definition of an object-free category, introducing the two properties: left composable and right composable, and a simplification of the notation through a symbol, a binary relation between morphisms, that indicates whether the composition is defined. In the final part we define two functions that allow to switch from the two definitions, with and without objects, and it is shown that their composition produces isomorphic categories.
The first four sections of this article include some auxiliary theorems related to number and finite sequence of numbers, in particular a primality test, the Pocklington's theorem (see ). The last section presents the formalization of Bertrand's postulate closely following the book , pp. 7-9.
The goal of this article is to formalize the Jordan-Hölder theorem in the context of group with operators as in the book . Accordingly, the article introduces the structure of group with operators and reformulates some theorems on a group already present in the Mizar Mathematical Library. Next, the article formalizes the Zassenhaus butterfly lemma and the Schreier refinement theorem, and defines the composition series.
The goal of this article is to formalize the Sylow theorems closely following the book . Accordingly, the article introduces the group operating on a set, the stabilizer, the orbits, the p-groups and the Sylow subgroups.
In this article, the principal n-th root of a complex number is defined, the Vieta's formulas for polynomial equations of degree 2, 3 and 4 are formalized. The solution of quadratic equations, the Cardan's solution of cubic equations and the Descartes-Euler solution of quartic equations in terms of their complex coefficients are also presented .
This article formalizes proofs of some elementary theorems of number theory (see [1, 26]): Wilson's theorem (that n is prime iff n > 1 and (n - 1)! ≅ -1 (mod n)), that all primes (1 mod 4) equal the sum of two squares, and two basic theorems of Euclid and Euler about perfect numbers. The article also formally defines Euler's sum of divisors function Φ, proves that Φ is multiplicative and that Σk|n Φ(k) = n.
The goal of this article is to formalize two versions of Ramsey's theorem. The theorems are not phrased in the usually pictorial representation of a coloured graph but use a set-theoretic terminology. After some useful lemma, the second section presents a generalization of Ramsey's theorem on infinite set closely following the book . The last section includes the formalization of the theorem in a more known version (see ).
The goal of this article is to formalize some theorems that are in the  on the web. These are elementary theorems included in every handbook of Euclidean geometry and trigonometry: the law of cosines, the Heron's formula, the isosceles triangle theorem, the intersecting chords theorem and the Ptolemy's theorem.
The main purpose of this article is to introduce the categorical concept of pullback in Mizar. In the first part of this article we redefine homsets, monomorphisms, epimorpshisms and isomorphisms  within a free-object category  and it is shown there that ordinal numbers can be considered as categories. Then the pullback is introduced in terms of its universal property and the Pullback Lemma is formalized . In the last part of the article we formalize the pullback of functors  and it is also shown that it is not possible to write an equivalent definition in the context of the previous Mizar formalization of category theory .
In the first part of this article we formalize the concepts of terminal and initial object, categorical product  and natural transformation within a free-object category . In particular, we show that this definition of natural transformation is equivalent to the standard definition . Then we introduce the exponential object using its universal property and we show the isomorphism between the exponential object of categories and the functor category .