diff --git a/metadata/entries/Berlekamp_Zassenhaus.toml b/metadata/entries/Berlekamp_Zassenhaus.toml
--- a/metadata/entries/Berlekamp_Zassenhaus.toml
+++ b/metadata/entries/Berlekamp_Zassenhaus.toml
@@ -1,49 +1,56 @@
title = "The Factorization Algorithm of Berlekamp and Zassenhaus"
date = 2016-10-14
topics = [
"Mathematics/Algebra",
]
abstract = """
We formalize the Berlekamp-Zassenhaus algorithm for factoring
square-free integer polynomials in Isabelle/HOL. We further adapt an
existing formalization of Yun’s square-free factorization algorithm to
integer polynomials, and thus provide an efficient and certified
factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and
then performs computations in the integer ring modulo p^k, where both
p and k are determined at runtime. Since a natural modeling of these
structures via dependent types is not possible in Isabelle/HOL, we
formalize the whole algorithm using Isabelle’s recent addition of
local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree
100 within seconds.
We formalize the Berlekamp-Zassenhaus algorithm for factoring
square-free integer polynomials in Isabelle/HOL. We further adapt an
existing formalization of Yun’s square-free factorization algorithm to
integer polynomials, and thus provide an efficient and certified
factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and
then performs computations in the integer ring modulo p^k, where both
p and k are determined at runtime. Since a natural modeling of these
structures via dependent types is not possible in Isabelle/HOL, we
formalize the whole algorithm using Isabelle’s recent addition of
local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree
100 within seconds.
+ Divasón, J., Joosten, S. J. C., Thiemann, R., & Yamada, A. (2019). A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm. Journal of Automated Reasoning, 64(4), 699–735. https://doi.org/10.1007/s10817-019-09526-y
+
+
+ von zur Gathen, J., & Gerhard, J. (2013). Modern Computer Algebra. https://doi.org/10.1017/cbo9781139856065
+
+
@article{Berlekamp_Zassenhaus-AFP,
author = {Jose Divasón and Sebastiaan J. C. Joosten and René Thiemann and Akihisa Yamada},
title = {The Factorization Algorithm of Berlekamp and Zassenhaus},
journal = {Archive of Formal Proofs},
month = {October},
year = {2016},
note = {\url{https://isa-afp.org/entries/Berlekamp_Zassenhaus.html},
Formal proof development},
ISSN = {2150-914x},
}
\ No newline at end of file
diff --git a/web/entries/Euler_Polyhedron_Formula.html b/web/entries/Euler_Polyhedron_Formula.html
--- a/web/entries/Euler_Polyhedron_Formula.html
+++ b/web/entries/Euler_Polyhedron_Formula.html
@@ -1,170 +1,172 @@
Euler's Polyhedron Formula - Archive of Formal Proofs
Euler stated in 1752 that every convex polyhedron satisfied the formula $V - E + F = 2$
where $V$, $E$ and $F$ are the numbers of its vertices, edges, and faces. For three dimensions,
the well-known proof involves removing one face and then flattening the remainder to form a planar graph,
which then is iteratively transformed to leave a single triangle. The history of that proof is extensively
discussed and elaborated by Imre Lakatos, leaving one finally wondering whether
the theorem even holds. The formal proof provided here has been ported from HOL Light,
where it is credited to Lawrence. The proof generalises Euler's observation
from solid polyhedra to convex polytopes of arbitrary dimension.
Lawrence, J. (1997). A Short Proof of Euler’s Relation for Convex Polytopes. Canadian Mathematical Bulletin, 40(4), 471–474. https://doi.org/10.4153/cmb-1997-056-4
+