# Re: [isabelle] bit vs. bool in HOL-Word

On Wed, Aug 21, 2013 at 8:57 AM, Stefan Berghofer <berghofe at in.tum.de> wrote:
> Hi Brian,
>
> could you describe in a bit more detail which aspects of finite fields
> you have formalized? In particular, have you formalized the concept of
> an irreducible polynomial, together with specific irreducibility criteria?

I haven't formalized very much: Polynomial.thy defines div, mod, and
gcd on univariate polynomials over a field, but I haven't formalized
irreducibility or proved any related theorems.

> When I started a formalization of AES a while ago, I used a brute-force
> approach to prove that the polynomial in the AES specification is actually
> irreducible. More precisely, to prove that p is irreducible I proved that
> no polynomial q with degree q \in {1..degree p div 2} divides p, but I was
> wondering whether there are more clever ways of doing this.

I guess there are ([1] suggests a few methods), but I don't know of
any formalizations of such methods in Isabelle.

[1] http://en.wikipedia.org/wiki/Factorization_of_polynomials_over_finite_fields

- Brian



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.