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.

""" license = "bsd" note = "" [authors] [authors.divason] homepage = "divason_homepage" [authors.joosten] email = "joosten_email" [authors.thiemann] email = "thiemann_email" [authors.yamada] email = "yamada_email" [contributors] [notify] thiemann = "thiemann_email" [history] [extra] [related] +dois = [ + "10.1007/s10817-019-09526-y", + "10.1017/CBO9781139856065" +] +pubs = [ + "Wikipedia" +] diff --git a/web/entries/Berlekamp_Zassenhaus.html b/web/entries/Berlekamp_Zassenhaus.html --- a/web/entries/Berlekamp_Zassenhaus.html +++ b/web/entries/Berlekamp_Zassenhaus.html @@ -1,243 +1,252 @@ The Factorization Algorithm of Berlekamp and Zassenhaus - Archive of Formal Proofs

The Factorization Algorithm of Berlekamp and Zassenhaus

Jose Divasón 🌐, Sebastiaan J. C. Joosten 📧, René Thiemann 📧 and Akihisa Yamada 📧

October 14, 2016

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.

License

BSD License

Topics

- +

Related publications

+
  • + 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 + +
  • + Wikipedia +

Session Berlekamp_Zassenhaus

Depends on

Used by

Auto-related entries

Cite

× 
@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},
 }
Download

Download

× Download latest

Older releases:

\ 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's Polyhedron Formula

Lawrence C. Paulson 📧

September 16, 2023

Abstract

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.

License

BSD License

Topics

Related publications

  • 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 +
  • + Wikipedia

Session Euler_Polyhedron_Formula

Cite

× 
@article{Euler_Polyhedron_Formula-AFP,
   author  = {Lawrence C. Paulson},
   title   = {Euler's Polyhedron Formula},
   journal = {Archive of Formal Proofs},
   month   = {September},
   year    = {2023},
   note    = {\url{https://isa-afp.org/entries/Euler_Polyhedron_Formula.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
Download

Download

× Download latest
\ No newline at end of file