EPiC Series in Computing

Volume 94, 2023, Pages 1–10

Proceedings of 24th International Conference on Logic
for Programming, Artificial Intelligence and Reasoning

Formalization of Algebraic Theorems in PVS∗

(Invited Talk)
Mauricio Ayala-Rincón1 , Thaynara Arielly de Lima2 , Andréia Borges
Avelar3 , and André Luiz Galdino4
1
Universidade de Brasília - Brasília D.F., Brasil
ayala@unb.br
2
Universidade Federal de Goiás - Goiás, Brasil
thaynaradelima@ufg.br
3
Universidade de Brasília - Planaltina, Brasil
andreiaavelar@unb.br
4
Universidade Federal de Catalão - Catalão, Brasil
andregaldino@ufcat.edu.br

Abstract
This talk discusses current extensions on the theory algebra from the NASA/PVSli-
brary on formal developments for the Prototype Verification System (PVS). It discusses
the approach to formalizing theorems of the ring theory and how they are applied to infer
properties of specific algebraic structures. As cases of study, we will present recent formal-
izations on the theories of Euclidean Domains and Quaternions. Moreover, we will show
how a general verification of Euclid’s division algorithm can be specialized to verify this
algorithm for specific Euclidean Domains, and how the abstract theory of Quaternions can
be parameterized to deal with the structure of Hamilton’s Quaternions.

1 Introduction
The PVS algebra library, part of the NASA/PVSlib, was recently enriched with a series of
theorems on rings. The extension includes complete formalizations of the isomorphism theorems
for rings, principal, prime, and maximal ideals, and an abstract version of the Chinese Remain-
der Theorem (CRT), which holds for abstract rings, even non-commutative rings. The benefit
of formalizing algebraic results from this abstract theoretical perspective was made evident by
showing how, from the abstract version of CRT, the formally verified well-known numerical
version of CRT for the ring of integers Z is obtained [6]. In this talk, we discuss another sub-
stantial step towards enriching the PVS abstract algebra library by formalizing properties about
factorization in commutative rings regarding both unique factorization domains, and Euclidean
rings [7]. Roughly, unique factorization domains are abstract structures for which a general
∗ Project supported by FAPDF DE 00193.00001175/21-11, CNPq Universal 409003/21-2, and FAPEG

202310267000223 grants. Speaker partially funded by CNPq grant 313290/21-0.

R. Piskac and A. Voronkov (eds.), LPAR 2023 (EPiC Series in Computing, vol. 94), pp. 1–10
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

version of the Fundamental Theorem of Arithmetic holds. On the other hand, Euclidean rings
are equipped with a norm that allows defining a suitable generalization of Euclid’s division
lemma and, therefore, of notions such as the greatest common divisor (gcd). The practicality
of gcd is well-known in the ring Z. Nevertheless, mathematicians know this notion is of general
fundamental importance in abstract Euclidean domains for which, in general, gcd should and
may be defined differently.
The primary motivation to formalize the theory of such structures is their theoretical and
practical application potential. For instance, a general abstract version of the Euclidean algo-
rithm can be specified to determine a gcd between sets of elements (Euclidean gcd algorithm)
in a Euclidean domain. Thus, since structures as the ring of integers Z, the Gaussian integers
Z[i], and rings of polynomials over integral domains are Euclidean domains, the Euclidean gcd
algorithm can be applied over them.
This document includes links to parts of the extended algebra theory in progress.

2 Formalization of Euclidean Domains and Algorithms

Notions such as prime element, division, and gcd between two elements and some landmark
results, including the Fundamental Theorem of Arithmetic, Euclid’s division lemma, and Eu-
clidean Algorithm, are well established and widespread for the ring of integers. These concepts
and general versions of exciting results are extended for abstract algebraic structures ([14], [8],
[9]) and are the scope of our formalization [6, 7].
The notions of prime and irreducible elements rely on the concept of divisibility on a ring.
The notions of divisibility and associated elements are specified as curried predicates abstracted
for any ring given as their first argument, R (ring_divides_def ).
In Hungerford’s textbook, the definition of divisibility relies on a commutative ring. It
avoids the discrimination between an element’s left or right divisor, and since the primary
results demand commutativity, it is a reasonable requirement. However, commutativity is not a
crucial property in such a notion since it only depends on the multiplication operation in a ring.
Because of that, we opted to generalize the definition and specify divisibility on non-necessarily
commutative rings as (divides?(R)(a,b) ). Another interesting remark is related to the
specification of associates?(R)(a,b) . Hungerford’s textbook omits that the type of the
parameters a and b are non-zero elements. Of course, this is obvious since it is required in the
definition of divides?(R)(a,b). However, the lack of such a hypothesis is recurrent in several
statements in the textbook (for instance, in Theorem 2.1).
In the sub-theory ring_divides , we formalized the properties related to the divisibility
stated in Theorem 2.1. Some of them involve the object “unit”. In a ring (R, +, ∗, zero, one)
with multiplication identity one, an element u is called a unit if u is left- and right-invertible;
that is, if there exist elements u−1 −1 −1 −1
1 , u2 ∈ R such that u ∗ u1 = u2 ∗ u = one.

Theorem 2.1 (Th.3.2, Hungerford [14]). Let a, b and u be elements of a commutative ring R
with identity.
(i) a divides b (denoted as a | b) if and only if (b) ⊂ (a), where (x) denotes the principal ideal
generated by x.
(ii) a and b are associates if and only if (a) = (b).
(iii) u is a unit if and only if u | r for all r ∈ R.
(iv) u is a unit if and only if (u) = R.

2
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

(v) The relation “a and b are associates” is an equivalence relation on R.

(vi) If a = br, where r ∈ R is a unit, then a and b are associates. If R is an integral domain,
then the converse is true.

Theorem 2.1 has a straightforward formalization due to the robustness of the formal frame-
work previously developed for rings and principal ideals [6]. The formalization of the properties
(i), (ii), and (iv) illustrates it clearly. In fact, by definition, (a) denotes the intersection of
all ideals in a ring R containing the element a. The lemma principal_ideal_charac in
theory ring_principal_ideal characterizes (a) as the set one_gen(R)(a) in the the-
ory ring_one_generator. The last characterization depends on a sum, specified as R_sigma,
over elements of a function in the ring R, defined over abstract types, as given in the theory
ring_basic_properties . The constructor R_sigma generalizes constructors in the PVSlib
built for specific theories as the theory of reals. Also, since R is a commutative ring with identity,
the lemma commutative_id_one_gen_charac provides a much simpler characterization of
the set one_gen(R)(a); indeed, such characterization simplifies the analysis of properties (i),
(ii), and (iv) since (a) can be built as the set aR = {ar : r ∈ R}.
From the concepts of divisibility and unit, we specified prime and irreducible ele-
ments on a ring with identity as the predicates ring_irreducible_element_def and
ring_prime_element_def , respectively.
In the ring of integers, prime and irreducible elements are indistinguishable. However, this
is not true for all rings. For instance, 2 is prime but not irreducible in Z6 . Theorem 2.2
gives some properties regarding prime and irreducible elements formalized in the subtheories
ring_prime_element and ring_principal_ideal_domain . Among others, it shows
that prime and irreducible elements are equal over principal ideal domains.

Theorem 2.2 (Th.3.4, Hungerford [14]). Let p and c be nonzero elements in an integral domain
R.

(i) p is prime if and only if (p) is a nonzero prime ideal;

(ii) c is irreducible if and only if (c) is maximal in the set S of all proper principal ideals of
R.

(iii) Every prime element of R is irreducible.

(iv) If R is a principal ideal domain, then p is prime if and only if p is irreducible.

(v) Every associate of an irreducible [resp. prime] element of R is irreducible [resp. prime].

(vi) The only divisors of an irreducible element of R are its associates and the units of R.

Hungerford stated the result for integral domains but advised that a weakened hypothesis
can be considered in some parts of the theorem. We formalize the results using the minimum
number of required conditions and detect that items (i) and (vi) hold for commutative rings
with identity.
Properties (i), (ii), and (iii) form the basis for the formalization of the characterization of
primes as irreducible elements over principal ideal domains, given in property (iv) and specified
as the lemma PID_prime_el_iff_irreducible .
It is important to stress here that in the pen-and-paper proof of property (iv) given in [14],
Hungerford assumes the vital result that maximal elements in the previously mentioned set S

3
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

are maximal ideals in R. We formalized this property without this assumption as the lemma
el_max_iff_one_gen_maximal in the sub-theory ring_principal_ideal_domain.
The Fundamental Theorem of Arithmetic for integers states that any positive integer
greater than 1 can be factorized as a unique product of primes. Unique Factorization Do-
mains (UFDs) are integral domains satisfying an analogous to this theorem. The specification
ring_unique_factorization_domain_def depends on a sequence of irreducible elements
fsIr?(R)(fsI) on a ring R with identity and a recursive operator op_fseq(fsI), as specified
in the sub-theory op_finseq_def , which multiplies the elements of such a sequence. The
operator op_fseq(fsI) is specified over an abstract structure (T, ∗, one) equipped with a binary
operation ∗ and a constant one.
Such a general specification is very useful for formalization matters for two reasons. Firstly,
it allows the use of the operator op_fseq(fsI) in a variety of abstract and concrete structures
(monoids, monads, groups, rings, integers, reals) by only adequately parameterizing the sub-
theory op_finseq_def. Secondly, it reduces proof obligations, called in PVS Type Correctness
Conditions (TCCs), automatically generated by the system, since the operator is defined for
elements of an abstract type, increasing the grade of automation.
In sub-theory ring_unique_factorization_domain , we formalized the landmark The-
orem 2.3 about UFDs.

Theorem 2.3 (Th.3.7, Hungerford [14]). Every principal ideal domain is a unique factorization
domain.

The formalization of the Theorem 2.3 consists in proving the existence and uniqueness of a
factorization as detailed in [7].
A Euclidean ring is a commutative ring R with a norm φ over R − {zero}, where an
abstract version of the well-known Euclid’s division lemma holds. Euclidean rings and domains
are specified in the subtheories euclidean_ring_def and euclidean_domain_def .
The fact that elements of Euclidean rings can be factorized as irreducible elements is for-
malized as Theorem 2.4, in sub-theory euclidean_domain .

Theorem 2.4 (Th.3.9, Hungerford [14]). A Euclidean ring R is a principal ideal ring with
identity. Consequently, every Euclidean domain is a unique factorization domain.

The proof of this theorem applies the well-ordering principle over φ(I ∗ ) = {φ(x) ∈ N; x ∈
I − {zero}}, where I is a nonzero ideal in R and φ is a norm on R − {zero}. By choosing a ∈ I
such that φ(a) is the minimum element of φ(I ∗ ), b ∈ I satisfies b = qa + r, for some q ∈ R
and r ∈ I. From this, one infers that r = 0, since r ̸= 0 contradicts the minimality of φ(a).
Therefore, b = qa and I ⊂ Ra ⊂ (a) ⊂ I imply that every ideal in R is a principal ideal. By
Theorem 2.3, one has that a Euclidean principal ideal domain is a unique factorization domain.
In sub-theory euclidean_domain , we also formalized the results stating that the ring
of integers ( ) and any arbitrary field ( ) are Euclidean domains.

3 Formalization of gcd Algorithm for Euclidean Domains

The theory Euclidean_ring_def includes two definitions that abstract Euclidean norms
and associated functions fulfilling the properties of Euclidean rings.
The first definition is the relation Euclidean_pair? Given a Euclidean ring R and a Eu-
clidean norm of non-zero elements over the naturals ϕ : R\{zero} → N, Euclidean_pair?(R, ϕ)
holds if ϕ satisfies the constraints of a Euclidean norm over R.

4
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

The second definition is the curried relation Euclidean_f_phi?(R, ϕ)(fϕ ) . This relation
holds if Euclidean_pair?(R, ϕ) does, and fϕ is a function from R × R \ {zero} to R × R, such
that for all pair of elements of R in its domain, fϕ (a, b) gives a pair of elements, say (div, rem)
satisfying the constraints of Euclidean rings for the norm ϕ: if a ̸= zero, a = div ∗ b + rem, and
if rem ̸= zero, ϕ(rem) < ϕ(b).
Both definitions are correct since the existence of such a ϕ and fϕ is guaranteed by the fact
that R is a Euclidean ring. Also, notice that the decrement of the norm, i.e., ϕ(rem) < ϕ(b), is
the key to implementing an abstract Euclidean terminating procedure.
The Euclidean gcd algorithm is specified in the sub-theory ring_euclidean_algorithm
as the curried definition Euclidean_gcd_algorithm . The types of its arguments guaran-
tee the correctness of this algorithm. Indeed, since the arguments R, ϕ, and fϕ should satisfy
Euclidean_f_phi?(R, ϕ)(fϕ ), R is a Euclidean ring with associated Euclidean norm ϕ and
adequate division and remainder functions given by fϕ . The termination of the algorithm is
obtained by discharging a proof obligation (termination TCC) generated by PVS. Termina-
tion is proved using the lexicographical MEASURE in the algorithm specification that decreases
after each possible recursive call. For Euclidean_gcd_algorithm(R, ϕ, fϕ )(a, b), if a ̸= zero,
ϕ(a) ≥ ϕ(b) and rem ̸= zero, the recursive call is Euclidean_gcd_algorithm(R, ϕ, fϕ )(b, rem),
and (ϕ(b), ϕ(a)) is greater than (ϕ(rem), ϕ(b)), since ϕ(b) > ϕ(rem). In the other case, if
a ̸= zero, and ϕ(b) > ϕ(a), the recursive call is Euclidean_gcd_algorithm(R, ϕ, fϕ )(b, a), and
(ϕ(b), ϕ(a)) is greater than (ϕ(a), ϕ(b)).
The correctness proof results as a corollary of the Euclid_theorem . It states the cor-
rectness of each recursive step regarding the definition of gcd given in Specification 1.
Essentially, this theorem states that given a Euclidean norm ϕ and associated function fϕ , the
gcd of a pair (a, b) is equal to the gcd of the pair (rem, b), where rem is computed as the second
projection of fϕ (a, b). Notice that since Euclidean rings allow a variety of Euclidean norms and
associated functions (e.g., [14], [9]), the definition of gcd is not specified as a function but as
the relation “gcd?”.
Finally, the theorem Euclidean_gcd_alg_correctness formalizes the correctness of the
Euclidean algorithm by induction, using the lexicographic MEASURE. For an input pair (a, b), in
the inductive step of the proof, when ϕ(b) > ϕ(a) and the recursive call swaps the arguments,
one assumes that

gcd?(R)({b, a}, Euclidean_gcd_algorithm(R, ϕ, fϕ )(b, a))

From this, one concludes that

gcd?(R)({a, b}, Euclidean_gcd_algorithm(R, ϕ, fϕ )(a, b)).

Otherwise, when the recursive call is Euclidean_gcd_algorithm(R, ϕ, fϕ )(b, rem), which hap-
pens if ϕ(a) ≥ ϕ(b), and rem is the second component of fϕ (a, b); by induction hypothesis one
has that
gcd?(R)({b, rem}, Euclidean_gcd_algorithm(R, ϕ, fϕ )(b, rem))
Finally, by application of Euclid_theorem, one concludes that the abstract general Euclidean
algorithm computes a gcd for the pair (a, b) correctly.
Now, we show how the correctness of the abstract algorithm Euclidean_gcd_algorithm is
easily inherited, under adequate parameterizations, for the structures of integers Z and Gaus-
sian integers Z[i]. The lines of reasoning follow those given in discussions on factorization in
commutative rings and multiplicative norms in textbooks (e.g., Section 47 in [9], or Chapter 3,
Section 3 in [14]).

5
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

Specification 1: gcd definition for commutative rings - sub-theory ring_gcd_def

gcd ?( R )( X : { X | NOT empty ?( X ) AND subset ?( X , R )} , d :( R - { zero })): bool =
( FORALL a : member (a , X ) IMPLIES divides ?( R )( d , a )) AND
( FORALL ( c :( R - { zero })):
( FORALL a : member (a , X ) IMPLIES divides ?( R )( c , a )) IMPLIES
divides ?( R )( c , d ))

Specification 2: Correctness of the parameterization of the abstract Euclidean algorithm for the
Euclidean ring Z - sub-theory ring_euclidean_gcd_algorithm_Z
phi _ Z ( i : int | i /= 0) : posnat = abs ( i )

f _ phi _ Z ( i : int , ( j : int | j /= 0)) : [ int , below [ abs ( j )]] =

(( IF j > 0 THEN ndiv (i , j ) ELSE - ndiv (i , - j ) ENDIF ) , rem ( abs ( j ))( i ))

phi _ Z _ and _ f _ phi _ Z _ ok : LEMMA Euclidean _ f _ phi ?[ int ,+ ,* ,0]( Z , phi _ Z )( f _ phi _ Z )

Euclidean _ gcd _ alg _ correctness _ in _ Z : COROLLARY

FORALL ( i : int , ( j : int | j /= 0) ) :
gcd ?[ int ,+ ,* ,0]( Z )({ x : ( Z ) | x = i OR x = j } ,
Euclidean _ gcd _ algorithm [ int ,+ ,* ,0 ,1]( Z , phi _Z , f _ phi _ Z )( i , j ))

For the Euclidean ring Z, the Euclidean norm ϕZ is selected as the absolute value while the
associated function fϕZ is built using the integer division and remainder, specified in the PVS
prelude libraries as div and rem: for a ∈ Z, b ∈ Z \ {0}, div(a, b) computes the integer division
of a by b, and, for b ∈ Z+ \ {0}, rem(b)(a) computes the remainder of a by b.
The correctness of the Euclidean algorithm for the ring of integers is specified as
the corollary Euclidean_gcd_alg_correctness_in_Z . It states that for the Euclidean
ring of integers Z, and any i, j ∈ Z, j ̸= 0, the parameterized abstract algorithm,
Euclidean_gcd_algorithm[int,+,*,0,1] satisfies the relation gcd?[int,+,*,0]:

gcd?[int, +, ∗, 0](Z)({i, j},

Euclidean_gcd_algorithm[int, +, ∗, 0, 1](Z, ϕZ , fϕZ )(i, j))
The proof of this corollary follows from the theorem of correctness for the abstract Eu-
clidean algorithm, Euclidean_gcd_alg_correctness. It requires proving that the chosen
Euclidean measure ϕZ , and the associated function fϕZ fulfill the conditions in the defini-
tion of Euclidean rings. The latter is formalized as lemma phi_Z_and_f_phi_Z_ok :
Euclidean_f_phi?[int, +, ∗, 0](Z, ϕZ )(fϕZ ).
For Gaussian integers, x = (Re(x) + i Im(x)) ∈ Z[i], the Euclidean norm, ϕZ[i] (x), is selected
as Re(x)2 + Im(x)2 . An adequate associated function fϕZ[i] (f_phi_Zi ) is specified through
the auxiliary function div_rem_appx . For a pair of integers (a, b), b ̸= 0, this function
computes the pair of integers (q, r) such that a = q b + r, and |r| ≤ |b|/2; thus, q b is the integer
closest to a. The equality a = q b + r is formalized as lemma div_rev_appx_correctness .
Now, we explain the construction of the function fϕZ[i] . For y, a Gaussian integer and
x, a positive integer, let Re(y) = q1 x + r1 and Im(y) = q2 x + r2 , where (q1 , r1 ) and (q2 , r2 )
are computed with the auxiliary function div_rem_appx (with respective inputs (Re(y), x) and
(Im(y), x)). Let q = q1 + iq2 and r = r1 + ir2 , then y = qx + r. Notice that if r ̸= 0 then
ϕZ[i] (r) ≤ ϕZ[i] (x), since r12 + r22 ≤ x2 /2 ≤ x2 . For the case in which x is a non zero Gaussian
integer, ϕZ[i] (x) > 0 holds.
Therefore, div_rem_appx(y conjugate(x), x conjugate(x)), where conjugate(x) = (Re(x)−

6
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

i Im(x)), can be computed obtaining q, r′ ∈ Z[i] such that y conjugate(x) = q (x conjugate(x))+

r′ , and r′ = 0 or ϕZ[i] (r′ ) < ϕZ[i] (x conjugate(x)).
By selecting r = y − q x, we obtain y = q x + r and r conjugate(x) = r′ .
Finally, when r ̸= 0, since ϕZ[i] (r conjugate(x)) < ϕZ[i] (x conjugate(x)), by application of
the lemma phi_Zi_is_multiplicative , we conclude that ϕZ[i] (r) < ϕZ[i] (x).
The formalization of the correctness of the Euclidean algorithm for Gaussian integers ob-
tained by parameterizations with Z[i], its Euclidean norm ϕZ[i] and associated function fϕZ[i]
follows as the simple corollary Euclidean_gcd_alg_ in_Zi . This is proved using the cor-
rectness of the abstract Euclidean algorithm and lemma phi_Zi_and_f_phi_Zi_ok . The
latter states that the Euclidean norm ϕZ[i] and its associated function fϕZ[i] are adequate for
the Euclidean ring Z[i]: Euclidean_f_phi?[complex, +, ∗, 0](Z[i], ϕZ[i] )(fϕZ[i] ).

4 The theory of Quaternions

The theory of quaternions is built from any field (specified in PVS as a commutative division
ring) over four-dimensional vector spaces ([x, y, z, t]).
The specification of quaternions uses an abstract type T with binary operators for an addi-
tion + and a multiplication ∗ over T, with identity elements zero and one, respectively. The
elements of type T with + and zero is a group. The specification includes axioms for quater-
nion addition and multiplication, including the quaternions axioms i2 = a, j 2 = b, for given
parameters, a and b of T , the associativity for quaternion multiplication, the distributivity of
addition on multiplication; and, properties for the scalar product between elements of type T
and quaternions. All that is provided in the theory quaternion_def . At this point, no
additional properties on T are assumed.
Furthermore, in the PVS theory quaternions , using these axioms, and assuming T with
+, ∗, zero, and one is a field, a series of properties of the theory of quaternions are formalized.
These properties include the characterization of quaternion multiplication (q_prod_charac
); the fact that quaternions are a ring with unity (quat_is_ring_w_one ); and the charac-
terization of quaternions as division rings (quat_div_ring_char ).
Typical results on the theory of quaternions also include equalities as the ones below, where
p, q are quaternions, and p̄ denotes the conjugate of p given as [p’x, -p’y, -p’z, -p’t].
pq = q̄ p̄
q q̄ = q̄q
|q̄| = |q|
|pq| = |p||q|
q −1 = q̄/|q|2 , whenever the quaternion algebra is a division ring.
A quaternion algebra is a division ring whenever all non-zero element q satisfies q̄q ̸= zeroq .
Characterizing quaternions as division rings requires that the parameter ring have charac-
teristics different from two. Under this constraint, it is possible to prove that:

∀x, y ∈ T : ax2 + by 2 ̸= one =⇒ ∀t ∈ T : t2 + a−1 ̸= zero

From this, under the same constraint, it is possible to prove that:

∀x, y ∈ T : ax2 + by 2 ̸= one =⇒ ∀t ∈ T : at2 + b ̸= zero

Finally, under this constraint, we obtain the characterization of quaternions as division
rings:

7
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

∀x, y ∈ T : ax2 + by 2 ̸= one ⇐⇒ division_ring?[quat, +, ∗, zeroq , oneq ](fullset[quat])

Once again, following the general approach to specifying quaternions from abstract fields,
we can obtain specific quaternions as the well-known Hamilton’s quaternions. For this, the
theory of quaternions is imported, using the field of reals as a parameter, and the real −1 for
the parameters a and b: IMPORTING quaternions[real,+,*,0,1,-1,-1].

5 Related Work and conclusions

5.1 Related work
Several formalizations focus on specific ring structures as the ring of integers. Such developments
range from simple formalization exercises, such as correctness proofs of gcd algorithms for Z, to
elaborated mechanical proofs of the Chinese Remainder theorem for Z. The latter started from
Zhang and Hua’s RRL (Rewrite Rule Laboratory) mechanization [24], followed by different
approaches in Mizar, HOL Light, hol98, Coq [22], ACL2 [20], and VeriFun [23]. Nevertheless,
the general algebraic abstract approach is followed by a few developments. Such an approach
is followed in the Isabelle/HOL Algebra Library (see [2], [1], and [3]). Also, the Lean mathlib
library [17] formalizes that a Euclidean domain is a principal ideal domain and a principal ideal
domain is a unique factorization domain. The former is given as formally verified construction
from a definition. From this instance, it is possible to infer that the Gaussian integers are a
Euclidean domain and thus a principal ideal. Also, the Euclidean algorithm can be adapted to
structures as the Gaussian integers.
In Coq, results about groups, rings, and ordered fields were formalized as part of the FTA
project [11]; this work gave rise to the formalization of the Feit and Thompson’s proof of
the Odd Order Theorem [12]. Also, there are formalizations of real ordered fields [5], finite
fields [19], and rings with explicit divisibility [4]. In Nuprl and Mizar, there are proofs of the
Binomial Theorem for rings in [15] and [21], respectively, and a Mizar formalization of the First
Isomorphism Theorem for rings [16]. ACL2 provides a hierarchy of algebraic structures ranging
from setoids to vector spaces that aims the formalization of computer algebra systems [13].
There are formalizations of Hamilton’s quaternions in HOL Light and Isabelle/HOL (e.g.,
[10], [18]). In contrast, some elements of the general theory of quaternions built over any
abstract field, as in our case, were developed as part of the Lean mathlib library [17].

5.2 Conclusions
In contrast to other works, restricted to specific ring structures, our formalization approach
focuses on the theory of abstract rings, as done in the Lean- and Isabelle-related libraries (cf
[17], and [3], respectively) discussed in the related work. Advantages of such an approach
include increasing the interest of mathematicians in formalizations and having practical general
presentations of computational algebraic properties portable to specific ring structures.

References
[1] Jesús Aransay, Clemens Ballarin, Martin Baillon, Paulo Emílio de Vilhena, Stephan Hohe, Flo-
rian Kammüller, and Lawrence C. Paulson. The Isabelle/HOL Algebra Library. Technical re-

8
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

port, Isabelle Library, University of Cambridge Computer Laboratory and Technische Universität
München, June 2019.
[2] Jesús Aransay and Jose Divasón. Formalisation of the computation of the echelon form of a matrix
in isabelle/hol. Formal Aspects Comput., 28(6):1005–1026, 2016.
[3] Clemens Ballarin. Exploring the structure of an algebra text with locales. Journal of Automated
Reasoning, 64:1093–1121, 2019.
[4] Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, and Vincent Siles. Formalized
linear algebra over Elementary Divisor Rings in Coq. Logical Methods in Computer Science,
12(2:7):1–23, June 2016.
[5] Cyril Cohen and Assia Mahboubi. Formal proofs in real algebraic geometry: from ordered fields
to quantifier elimination. Logical Methods in Computer Science, 8(1:2):1–40, 2012.
[6] Thaynara Arielly de Lima, André Luiz Galdino, Andréia Borges Avelar, and Mauricio Ayala-
Rincón. Formalization of Ring Theory in PVS - Isomorphism Theorems, Principal, Prime and
Maximal Ideals, Chinese Remainder Theorem. J. Autom. Reason., 65(8):1231–1263, 2021.
[7] Thaynara Arielly de Lima, André Luiz Galdino, Andréia Borges Avelar, and Mauricio Ayala-
Rincón. Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms.
Technical report, Universidade de Brasília, Departments of Mathematics and CS, Brasília D.F.,
2023. Accepted in LSFA 2023.
[8] David S. Dummit and Richard M. Foote. Abstract Algebra. Wiley, 3 edition, July 2003.
[9] John B. Fraleigh. A First Course in Abstract Algebra. Pearson, 7th edition, 2003.
[10] Andrea Gabrielli and Marco Maggesi. Formalizing Basic Quaternionic Analysis. In Proc. 8th
International Conference on Interactive Theorem Proving ITP, volume 10499 of Lecture Notes in
Computer Science, pages 225–240. Springer, 2017.
[11] Herman Geuvers, Randy Pollack, Freek Wiedijk, and Jan Zwanenburg. A constructive algebraic
hierarchy in Coq. Journal of Symbolic Computation, 34(4):271–286, 2002.
[12] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot,
Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence
Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A Machine-Checked Proof of the Odd
Order Theorem. In 4th International Conference on Interactive Theorem Proving ITP, volume
7998 of Lecture Notes in Computer Science, pages 163–179. Springer, 2013.
[13] Jónathan Heras, Francisco Jesús Martín-Mateos, and Vico Pascual. Modelling algebraic structures
and morphisms in ACL2. Applicable Algebra in Engineering, Communication and Computing,
26(3):277–303, Jun 2015.
[14] Thomas W. Hungerford. Algebra, volume 73 of Graduate Texts in Mathematics. Springer-Verlag,
New York-Berlin, 1980. Reprint of the 1974 original.
[15] Paul Bernard Jackson. Enhancing the Nuprl Proof Development System and Applying it to Com-
putational Abstract Algebra. PhD thesis, Cornell University, 1995.
[16] Artur Kornilowicz and Christoph Schwarzweller. The First Isomorphism Theorem and Other
Properties of Rings. Formalized Mathematics, 22(4):291– 301, 2014.
[17] The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIG-
PLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367–381.
ACM, 2020.
[18] Lawrence C. Paulson. Quaternions. Arch. Formal Proofs, 2018, 2018.
[19] Jade Philipoom. Correct-by-Construction Finite Field Arithmetic in Coq. Master’s thesis, Master
of Engineering in Computer Science, MIT, 2018.
[20] David M. Russinoff. A Mechanical Proof of the Chinese Remainder Theorem. UTCS Technical
Report - no longer available - ACL2 Workshop 2000 TR-00-29, University of Texas at Austin,
2000.
[21] Christoph Schwarzweller. The Binomial Theorem for Algebraic Structures. Journal of Formalized

9
Formalizing Factorization on Euclidean Domains - IT M. Ayala-Rincón et al.

Mathematics, 12(3):559–564, 2003.

[22] Christoph Schwarzweller. The Chinese Remainder Theorem, its Proofs and its Generalizations in
Mathematical Repositories. Studies in Logic, Grammar and Rhetoric, 18(31):103–119, 2009.
[23] Christoph Walther. A Machine Assisted Proof of the Chinese Remainder Theorem. Technical
Report VFR 18/03, FB Informatik, Technische Universität Darmstadt, 2018.
[24] Hantao Zhang and Xin Hua. Proving the Chinese Remainder Theorem by the Cover Set Induction.
In 11th International Conference on Automated Deduction CADE, volume 607 of Lecture Notes in
Computer Science, pages 431–445. Springer, 1992.

10