## My research and investigations

### Fermat’s Little Theorem

I have a joint paper with my supervisor, on combinatoric and group-theoretic proofs of Fermat’s Little Theorem in HOL4.

It all started when I came across the Necklace proof of Fermat’s Little Theorem, which is different from the textbook number-theoretic proof. The number-theoretic proof is also standard in automatic theorem provers, e.g. it is a worked example in HOL Light Tutorial. I was wondering how to put a combinatoric proof in HOL4.

It turns out that it is just a matter of counting with sets. There are tricks to set up bijections to establish the sizes of sets. Digging deeper, I find that there is a kind of symmetry underlying the bijections, and I am surprised to find group action is involved. Eventually I use the Orbit-Stabilizer Theorem to prove the Necklace Theorem, thereby proving Fermat’s Little Theorem.

At the end, we did several proofs of the theorem in HOL4, made a comparison, and gave the paper this title: “A String of Pearls: Proofs of Fermat’s Little Theorem”. The paper was accepted by CPP 2012, and I gave a talk at the conference held in Kyoto this December.

During this process, I have build up a library of group theory in HOL4. This should help my further work in finite fields.

### Software Bugs and Theorem Proving

Apple iPhone users are greeted with a silent alarm at the first day of 2011 (see here and here). All evidence points to a software bug in the operating system.

This is not the first widespread software bug from a well-known manufacturer. In 1994, a math professor found that the Intel Pentium CPU had a bug when doing divisions. It caused a sensation in the IT world (see here), and ultimately Intel recalled all flawed processors.

All modern electronic devices (your desktop, laptop, notebook, netbook, digital camera, mobile phone, mp3 player, etc.) contain software. These software are designed and implemented by smart engineers, and checked and tested by a team of testers. The aim is to get rid of every last software bug. After all these rigorous processes the software is 99.99999% correct — but it is the 0.00001% that embarrasses the company.

The only way to claim the perfect 100% is to prove it, mathematically. This means translating the design and implementation into the language of math, and to show that the implementation follows logically from the design. This is tedious work, not usually done by a human mathematician. Rather it is the job for theorem-provers, special programs that can perform automated reasoning.

You’ve probably never heard of these terms. It’s because traditionally theorem-provers exist only in universities, for academics doing research in automated theorem proving. Since the Pentium bug, hardware companies (like AMD) are relying on theorem-provers to verify microprocessor designs. Even software companies (like Microsoft) are doing research in theorem proving.

Now if you put on your logic hat, you’ll find an interesting situation: theorem-provers are themselves software coded by human, how can we be sure that theorem-provers don’t have bugs?

The answer is: we can’t be sure, but we do take measures to reduce the chance of any bugs.

Firstly, theorem-provers have a very small core, call the inference engine. Basically, it is capable of manipulating symbols, according to a few simple rules. Keeping everything simple means less hiding spots for bugs. The system starts with a few fundamental math facts (like every number has a next one), and requires any additional facts must be first proved by the inference engine. Thus the system builds up its power on a firm basis.

Secondly, theorem-provers are open-source projects. This means the source code of system, in particular its core inference engine, is open for inspection. In these days of Internet, you can download the source code. With appropriate tools, you can compile the codes and run the system in your own computer. People with like interest in the system will form a group checking the merits of the system, and contribute to any bug-fix or improvement of the source code. There is a saying in IT community: “given enough eyeballs, all bugs are shallow”.

The theorem-prover I’m using for my project is HOL4, which is open-source with a small core. Here is a readable introduction, and here is a technical overview.

My supervisor is one of the main developers of HOL4.

### Refreshing Childhood Math

To most people, math is something they learned in the days gone by.

I suppose children like math, especially the smart ones. Then the math puzzles become more puzzling, the math problems become more problematic. Struggling on, the flood of math formula is overflowing, any initial interest in math is washed away. When calculations turn into calculus, most will surrender. By the time we can exit from the education system, we are glad to say goodbye to math.

Life goes on. We don’t need calculus to find a job. There’s no formula to remember in daily matters. The tax calculations may pose a challenge, but now you’ve got a calculator. Most likely you’ve picked up a Rubik’s Cube, then put it down. In spare time you may enjoy a game of Sudoku. Isn’t life wonderful?

The world also moves on. Space travel requires complex calculations, but how to squeeze a computer, which can occupy a very big room in the 60s, into tiny spacecrafts? How to get pictures without films? How to communicate with a tiny robot millions of miles away with a dying battery? These are some of the challenges to scientists, and the solutions, by applying a lot of math, give birth to the current technology of laptops, digital cameras, image formats like JPEG, error-correction codes and the wireless communication network. Isn’t math wonderful?

To revive your childhood interest in math, physics and astronomy, you may like this recent (October 2010) Einstein Public Lecture by Terence Tao.

He described the lecture in his blog: The Cosmic Distance Ladder (version 4.1). There you can download the lecture in PDF or PPT, even his earlier versions. If your internet connection can handle the bandwidth, you can watch this lecture video. Being a public lecture, detailed calculations are omitted. If you need to see them there is a link from his earlier lecture in 2007.

Terence Tao (陶哲軒) has won many honors and awards, including a Fields Medal in 2006 – the math Nobel prize.

If you’d like to take a look at his current research (in math), click “Home” in his blog.

I did that, but didn’t get anything into my head. But then I sit back, and think, “What a nice idea, a blog talking about your own research.” When I start my research, I immediately sign up for WordPress.

### What Exactly Are You Doing

People close to me are excited by my pursue of PhD, and this is the question they’d like to know the answer.

Imagine a group of people gather around me. When I say “It’s a math topic”, half will leave. When I add “in automated reasoning”, another half will leave.

Math is one of the main subjects in education, and we do math everyday (how much is 30% off), but few are interested in math upon leaving school. Most think of math as calculations, which can be tedious. Some may be remember the tricky math problems, only the smart ones can solve them. Others may recall the frustration with math proofs, and conclude that proving math should be reserved for those with a different brain structure.

So, how am I going to explain what I’m doing to ordinary folks?

I think I’ll start with something everyone is now familiar with — sending text messages, via a mobile phone or the computer.

Once the message is sent, the words, which are symbols, are converted into numbers. There are several levels of this conversion:

• the first level is rather like old-fashion telegraph, where alphabets are coded into digital patterns. Although the details are a bit involved, they are essentially similar to putting A=1, B=2, C=3, etc.
• the second level is about secrecy. The message is supposed not to be readable by a third party, so the coded alphabets will be scrambled in a certain way, called encryption. When the numbers reach the other end, they will be unscrambled, reversing the encryption process, called decryption, so the recipient can read the message.
• the third level is about transmission. In order for the encrypted numbers to be reliably transmitted through a path that is not expected to be error-free, some extra information, or redundancy, are inserted to enable the receiving end to, at least, check if an error has occurred, and, preferably, to recover the intended numbers by a process called error-correction.

These underlying processes in message conversion clearly show that symbols are being handled as numbers, probably in ways you’ve never imagined — all these things happen at the push of a button! All these levels need math, both the theory to show why the method works, and the computations to actually carry out the processes.

On the other hand, numbers are just special symbols. Most civilizations used one-stroke for 1, two-strokes for 2, and three-strokes for 3. After that, the problem “how many more symbols should be invented?” becomes a struggle to the civilization. Even today we keep inventing prefixes – like K for kilo, M for mega, G for giga, T for tera — to describe larger and larger amounts. The name “Google” originates from a misspelling of “googol”, a number represented by a 1 followed by 100-zeros.

Looking at numbers as symbols is a shift in perspective. Once you take this view, math computations become symbolic manipulations: follow rules to move symbols around. That’s what computations really are. By doing so, computers can “compute” a lot of things: the pixels to give a picture, the sound to play a song, both color and sound to play a video. All information are symbols.

Back to math. Besides computations, math people are busy with another activity: proving theorems. On the surface, the process involves reasoning in logic; but most mathematicians hold the view that the reasoning steps can be broken down into elementary rules of moving logical symbols around. Hence, taking another shift in perspective, it is possible to do math proofs by math computations. This technique is called “automated reasoning”.

My project is to apply automated reasoning to investigate a well-known method in modern day communication. The method is used in error-correction of signal transmissions, e.g. wireless networks (Wi-Fi). The method is also used in efficient generation of random-looking bits for signal encryption (in mobile phones) as well as signal synchronization (in GPS devices). The fact that this method can be used in many different ways is fascinating. I would like to show clearly what is the shift in perspective behind the scene.

It is by shifting of perspective that researchers reveal new ways of looking at things. Sometimes these new ways of looking can lead to new ideas, enabling advance in technology. The IT revolution of the past decades is evidence of this happening — researchers solve various technical problems by shifting of perspective.