### Theorem-Proving in Finite Fields

This is my PhD project proposal.

## Introduction

Finite fields are also known as Galois fields, in honor of the French mathematical genius Évariste Galois (1811 – 1832). The theory is developed from a small list of axioms, with subject matter intimately related to the arithmetic of remainders under division. Division by prime numbers give base fields, while division by primitive polynomials give nice extensions of base fields. Such is the power of a simple theory, unifying ideas from diverse topics.

There are many theorems, big and small, in the theory of Finite Fields. Since axioms are very low-level, but theorems can be high-level, the chain of reasoning from axioms to theorems is often very long. It is not uncommon to find in textbooks proof sketches of high-level theorems, leaving tedious details as exercises. Such tasks are better suited to a theorem-prover, working tirelessly and attending to logical details.

## Applications

Although a topic in abstract algebra, Finite Fields have found applications in digital computers and digital communication. Two areas of interest to this project are:

**Linear Feedback Shift Register (LFSR)**– this is a simple logical circuit to deliver a sequence of binary bits. The bits look random: but since the number of circuit states is finite, the bits will repeat after a period. For cryptography, where long pseudo-random sequences can provide security for encryption, the problem is how to design LFSRs with long periods. Such work is pioneered by Solomon Golomb in 1955, showing the best LFSR designs are related to primitive polynomials in finite fields. Nowadays, LFSR have extensive military, industrial and consumer applications. For example, A5/1, a stream cipher used to encrypt mobile phone conversations in GSM standard, is LFSR-based (see here). Global Positioning System (GPS) uses an LFSR to rapidly transmit a sequence that indicates high-precision relative time offsets.**Error-Correcting Codes (ECC)**– these are coding schemes for reliable communication through a noisy channel. Examples are Bose-Chaudhuri-Hocquenghem (BCH) codes, which are based on primitive polynomials over a finite field. Because BCH codes can detect and correct multiple error bits, they are crucial for digital data storage and retrieval, and make NASA space missions possible. Reed-Solomon codes, a special type of BCH code, was used in Voyager 2 probe to send back color pictures of inner and outer planets. Today (see here) Reed-Solomon codes can be found in devices using CDs, DVDs, Blu-ray Discs; in hard-drives and flash-drives; as well as in communication protocols over networks, both cable and wireless.

The BCH codes and Reed-Solomon codes were conceived around 1960. Initially there is one drawback: while the codes can encode messages fast, the decoding process is complex and slow. In 1967, Elwyn Berlekamp invented an efficient algorithm for decoding BCH codes. Later in 1969, James Massey developed an algorithm for a different problem: how to find the shortest LFSR for given a binary sequence. Massey soon realized that his algorithm was essentially an improved version of Berlekamp’s algorithm. This Berlekamp-Massey algorithm, based on the theory of finite fields, turns using Reed-Solomon codes in error-detection and error-recovery a practical reality.

## Proposal

I intend to work on the formalization of Finite Fields, with the goal of proving Berlekamp-Massey algorithm. Major milestones are:

- Formalize elementary field theory from its axioms, based upon a finite set.
- Extend this formalization to include primitive polynomials of finite fields.
- Prove properties of LFSR within this finite fields formalization.
- Prove properties of BCH codes within this finite fields formalization.
- Show that the problems of BCH decoding and shortest LFSR are equivalent.
- Show that Berlekamp-Massey algorithm is correct.

### Notes

- The theorem-prover to be used is HOL4, a system with some packages for group theory and number theory.
- This formalization only covers the fundamental parts of the theory of Finite Fields.