In abstract algebra, a field is a system within which add, subtract, multiply and divide are possible. An example of such a system is all the fractions (called rationals Q in math), but the number of fractions is infinite. Finite systems with suitably-defined +-*/ do exist, and they are known as finite fields. It was a remarkable discovery by Évariste Galois, a math genius, that finite fields are characterized only by its number of elements, which must be either a prime or power of a prime. Due to this, finite fields are also known as Galois fields.
Finite fields have many practical applications, including cryptography, error-correcting codes and LFSRs (Linear feedback shift register) for pseudo-random number generation. There is a large collection of algorithms based on theory of finite fields.
Search on Net shows the Google project: coq-galois-theory. Its timeline suggests that some progress have been made, but still a lot of work to be done. Maybe I can do a project on proving/verifying finite field algorithms in error codes and LFSRs.