Mathematics and computer-assisted proofs

Mathematics and computers

Formal mathematics is something that some people see as a pen and paper endeavor, where a single mathematician is solving problems by hand, and the computer is only marginally used for doing big calculations or statistical analyses. While it is true that computers are used on the previously mentioned situations, computers can do much more in relation to mathematics. In fact, computers have been used to prove some interesting theorems:

  • Four-color theorem: Given any separation of a plane into contiguous (i.e., next to each other) regions, producing a figure called map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color.

  • Lorenz attractor: (I’m not explaining this… It is related to chaos theory and I am in no way an expert on this).

  • Kepler conjecture (now theorem): No arrangement of equally sized spheres filling space has a greater average density than that of the cubic close packing (face-centered cubic) and hexagonal close packing arrangement.

Among other theorems. Our objective here is then to argue that computers are actually good tools for working with formal mathematics. In particular, we will show how to formalize naive group theory in Coq and how we can mechanize the proof of some of the theorems.

Naive Group theory

The name naive group theory is a reference to the book Naive Set Theory by Paul Halmos, and which is an introduction for undergraduate students to set theory. What is interesting about the books is that Halmos omits one of the main axioms of Zermelo-Fraenkel Set Theory: the axiom of regularity, which guarantees that no set is a member of itself. Nonetheless, this is not a post on set theory; the main idea behind the name naive group theory is that we will only show a small formalization of the definition of a group and some of the axioms derived from there, hence, we will be omitting a lot of things that would be covered in a normal course in abstract algebra. This small tutorial presumes a bit of knowledge of the Coq proof assistant.

Main definitions and axioms

So let us start by laying out our definitions. A group is essentially a pair $(G,\oplus)$, where $G$ is a set and $\oplus$ is a binary operation between the elements of the set that satisfy certain axioms.

Definition 1. [Group]

Let $G$ be a set and $\oplus$ be an operation $\oplus: G \times G \rightarrow G$ that satisfies the following axioms:

  1. Closure: $\forall a,b \in G. (a \oplus b)\in G$.
  2. Neutral element: $\exists e\in G. \forall a\in G. a \oplus e = e = e \oplus a$.
  3. Inverses: $\forall a\in G. \exists b\in G. a \oplus b = e = b \oplus a$.
  4. Associativity: $\forall a,b,c\in G. (a \oplus b) \oplus c = a \oplus ( b \oplus c)$.

The previous definition is the standard definition of group. However, this definition is redundant. In fact, one can provide a definition with weaker axioms. Let’s see how this definition would be:

Definition 2. [Weak Group]

Let $G$ be a set and $\oplus$ be an operation $\oplus: G \times G \rightarrow G$ that satisfies the following axioms:

  1. Closure: $\forall a,b \in G. (a \oplus b)\in G$.
  2. Neutral element to the right: $\exists e\in G. \forall a\in G. a \oplus e = a$.
  3. Inverses to the right: $\forall a\in G. \exists b\in G. a \oplus b = e$.
  4. Associativity: $\forall a,b,c\in G. (a \oplus b) \oplus c = a \oplus ( b \oplus c)$.

Let us assume this definition for the sake of this tutorial, with a small tweak. Consider that the inverse is a function $i : G \rightarrow G$ that takes a single element from G and returns the inverse in $G$. We will explain why this later. Let us write $i(a)$ as $-a$, and assume that the neutral element will be $e$.

Now, our objective is then to prove the following theorems (the order is important, due to dependencies in the proofs):

  1. Theorem 1: $\forall a\in G. a \oplus a = e \Rightarrow a = e$.
  2. Theorem 2: $\forall a\in G. -a \oplus a = e$.
  3. Theorem 3: $\forall a\in G. e \oplus a = a$.
  4. Theorem 4: $\forall a,b,x\in G. a + x = b + x \Rightarrow a = b$.
  5. Theorem 5: $\forall a,b,x\in G. x + a = x + b \Rightarrow a = b$.
  6. Theorem 6: $\forall a,p. p\oplus a = a \Rightarrow p=e$.
  7. Theorem 7: $\forall a. b \oplus a = e \Rightarrow b = -a$.
  8. Theorem 8: $\forall a,p. a \oplus p = a \Rightarrow p=e$.
  9. Theorem 9: $\forall a. a \oplus b = e \Rightarrow b = -a$.
  10. Theorem 10: $\forall a,b \in G -(a\oplus b) = -a \oplus -b$.
  11. Theorem 11: $\forall a\in G. -(-a) = a$.
  12. Theorem 12 $-e = e$

Let us prove the first 2 theorems as an example. The interested reader may try to prove the rest.

Theorem 1:

$\forall a\in G. a \oplus a = e \Rightarrow a = e$.

Proof

Let us first analyze the statement by parts: for all $a\in G$. This means that it should be enough to consider an arbitrary $a$. Then we need to show that for the particular arbitrary $a$ we picked, this implication holds: $a \oplus a = e \Rightarrow a = e$. From here we assume that $a \oplus a = e$ and then, the reasoning is purely algebraic, considering that we can only use the 4 axioms we have. We start with the expression $a = e$. and work out the equality:

Theorem 2:

$\forall a\in G. -a \oplus a = e $.

Proof

We proceed, again, by assuming some $a\in G$ and we prove algebraically:

Note that the second step with $\rightsquigarrow$ means the following logical step: we want to prove $-a \oplus a = e$. Hence, if we can prove $(-a \oplus a) \oplus (-a \oplus a) = -a \oplus a$ we can apply Theorem 1 to finish the proof.

We have now shown, by hand, that two of the theorems are true. Now, we would like to implement this formalization plus the proofs we made, in Coq.

Naive group theory in Coq

Let us briefly mention what is Coq. The Coq proof assistant is a formal proof management system based on the Calculus of Constructions introduced and developed by Thierry Coquand under the supervision of Gérard Huet around 1988. The calculus of constructions is a formal language that can be used both as a typed programming language and via the Curry-Howard Isomorphism can also be used as a intuitionistic logical system that can be used to formalize the foundations of mathematics. I will not enter into much detail about this since I am not an expert. However, since Coq can be used to formalize mathematics, we can therefore formalize our small example.

The first step to formalize our example is to understand that the theory we previously formulated can be expressed all in terms of sets, functions and logical operators (these can also be seen as functions, but I’m not going down that rabbit hole). Let us consider a brief recap:

  1. Groups are pairs of sets and a single operation, which is defined as binary function that takes two elements from the group set and maps then a single element of the group set.
  2. There is a single element that belong to the set of the group.
  3. There is a unary function that takes a single element from $G$ and returns the inverse.
  4. All the axioms of set theory are presented as logic formulae.

Therefore, let us formalize step by step in Coq. First, we need to define what a group is. This is done as follows:

(* The set of the group. *)
Parameter G : Set.
(* The binary operator. *)
Parameter add : G -> G -> G.
(* The group identity. *)
Parameter e : G.
(* The inverse operator. *)
Parameter i : G -> G.

So, line by line: first, we define our set $G$ as a parameter of type Set, meaning that $G$ is a set… Ok, enough with the obvious. Then, we create a binary operator $add$. We say that $add$ has the type of a function that takes a single element from $G$ and then takes another element of $G$ and then returns an element of $G$. This way of writing a function with multiple parameters comes from a process called currying, but that is not the main issue of this tutorial. The third element for our set is the element $e$, the neutral element of the group. Finally, we define a function $i$ which will return the inverse of a given element from $G$.

After this we add to our Coq file some special code for readability:

Infix "+" := add (at level 50, left associativity).
Notation "¬ x" := (i x) (at level 75, right associativity).

The previous code will allow us to use $+$ as the binary operator, with left associativity and $\neg$ as the $-$ operator in the above proofs. Next, we define our axioms:

(*Associativity*)
Axiom assoc : forall a b c, (a + b) + c = a + (b + c).
(* Neutral to the right*)
Axiom neu_r : forall a, a + e = a.
(*Inverse to the right. *)
Axiom inv_r : forall a, a + (¬a) = e.

And now we can proof our first theorem:

Theorem unique_id : forall a, a + a = a -> a = e.
Proof.
intros.
rewrite <- neu_r with a.
rewrite <- inv_r with a.
rewrite <- assoc.
rewrite H.
reflexivity.
Qed.

When you execute this proof in coq, you can see that the followed steps are the same as the proof by hand that we made before. This is the interesting part, because Coq provides you with ways to write this. In particular, in this proof intros, allows you to assume the hypotheses and continue with the proof. Then, all the rewrites simply follow the steps of the proof we wrote previously.

Finally, we can proof the second theorem as follows:

Theorem inv_l : forall a, (¬a) + a = e.
Proof.
intros.
apply unique_id.
rewrite <- assoc with ((¬a) + a) (¬a) a.
rewrite assoc with (¬a) a (¬a).
rewrite -> inv_r with a.
rewrite -> neu_r with (¬a).
reflexivity.
Qed.

I will not publish the formalization of the proofs in full for all the theorems, since I have seen it is an exercise for some university courses.

Conclusions and disclaimers

I find very interesting the relation that exist between mathematical proofs and computers, as it becomes clear that computers are useful for doing much more than big calculations and statistical analyses of big data. Computers can also be useful tools for mathematicians that work on a very theoretical level on areas beyond the previously mentioned domains. I also believe that this is an important area for research, and thankfully, it is a very active are of research and with constant improvements being made to Coq and other proof assistants as well as the foundational theories that are behind them. Note however, that this small guide is in no way a full on manual to using Coq, nor a tutorial on group theory. There are so much more things to study in those topocs and several books have been written about them. All these books are easily found with a quick search on Google.

This post is based on the exercise published here.

Published: March 06 2018

  • category:
  • tags:
blog comments powered by Disqus