4-colour Theorem. Every planar graph is 4-colourable.

This theorem of course has a well-known history. It was first proven by Appel and Haken in 1976, but their proof was met with skepticism because it heavily relied on the use of computers. The situation was partially remedied 20 years later, when Robertson, Sanders, Seymour, and Thomas published a new proof of the theorem. This new proof still relied on computer analysis, but to such a lower extent that their proof was actually verifiable. Finally, in 2005, Gonthier and Werner used the Coq proof assistant to formalize a proof, so I suppose only the most die hard skeptics remain.

My question stems from reading this paper by Robin Thomas. In it, he describes several interesting reformulations of the 4-colour theorem. Here is one:

Note that the cross-product on vectors in $\mathbb{R}^3$ is not an associative operation. We therefore define a bracketing of a cross-product $v_1 \times \dots v_n$ to be a set of brackets which makes the product well-defined.

Theorem. Let $i, j, k$ be the standard unit vectors in $\mathbb{R}^3$. For any two different bracketings of the product $v_1 \times \dots \times v_n$, there is an assignment of $i,j,k$ to $v_1, \dots, v_n$ such that the two products are equal and non-zero.

The surprising fact is that this innocent looking theorem implies the 4-colour theorem.

Question. Is anyone working on an algebraic proof of the 4-colour theorem (say by trying to prove the above theorem)? If so, what techniques are involved? What partial progress has been made? Or do most people consider the effort/reward ratio of such an endeavor to be too high?

I think it would be interesting to have an algebraic proof, even a very long one, particularly if the algebraic proof does not use computers. Given its connection to many other areas (Temperley-Lieb Algebras), the problem seems to be amenable to other forms of attack.

4-colour Theorem. Every planar graph is 4-colourable.

This theorem of course has a well-known history. It was first proven by Appel and Haken in 1976, but their proof was met with skepticism because it heavily relied on the use of computers. The situation was partially remedied 20 years later, when Robertson, Sanders, Seymour, and Thomas published a new proof of the theorem. This new proof still relied on computer analysis, but to such a lower extent that their proof was actually verifiable. Finally, in 2005, Gonthier and Werner used the Coq proof assistant to formalize a proof, so I suppose only the most die hard skeptics remain.

My question stems from reading An Update on the Four-Color Theorem by Robin Thomas. The paper describes several interesting reformulations of the 4-colour theorem. Here is one:

Note that the cross-product on vectors in $\mathbb{R}^3$ is not an associative operation. We therefore define a bracketing of a cross-product $v_1 \times \dots v_n$ to be a set of brackets which makes the product well-defined.

Theorem. Let $i, j, k$ be the standard unit vectors in $\mathbb{R}^3$. For any two different bracketings of the product $v_1 \times \dots \times v_n$, there is an assignment of $i,j,k$ to $v_1, \dots, v_n$ such that the two products are equal and non-zero.

The surprising fact is that this innocent looking theorem implies the 4-colour theorem.

Question. Is anyone working on an algebraic proof of the 4-colour theorem (say by trying to prove the above theorem)? If so, what techniques are involved? What partial progress has been made? Or do most people consider the effort/reward ratio of such an endeavor to be too high?

I think it would be interesting to have an algebraic proof, even a very long one, particularly if the algebraic proof does not use computers. Given its connection to many other areas (Temperley-Lieb Algebras), the problem seems to be amenable to other forms of attack.

4-colour Theorem. Every planar graph is 4-colourable.

This theorem of course has a well-known history. It was first proven by Appel and Haken in 1976, but their proof was met with skepticism because it heavily relied on the use of computers. The situation was partially remedied 20 years later, when Robertson, Sanders, Seymour, and Thomas published a new proof of the theorem. This new proof still relied on computer analysis, but to such a lower extent that their proof was actually verifiable. Finally, in 2005, Gonthier and Werner used the Coq proof assistant to formalize a proof, so I suppose only the most die hard skeptics remain.

My question stems from reading this paper by Robin Thomas. In it, he describes several interesting reformulations of the 4-colour theorem. Here is one:

Note that the cross-product on vectors in $\mathbb{R}^3$ is not an associative operation. We therefore define a bracketing of a cross-product $v_1 \times \dots v_n$ to be a set of brackets which makes the product well-defined.

Theorem. Let $i, j, k$ be the standard unit vectors in $\mathbb{R}^3$. For any two different bracketings of the product $v_1 \times \dots \times v_n$, there is an assignment of $i,j,k$ to $v_1, \dots, v_n$ such that the two products are equal and non-zero.

The surprising fact is that this innocent looking theorem implies the 4-colour theorem.

Question. Is anyone working on an algebraic proof of the 4-colour theorem (say by trying to prove the above theorem)? If so, what techniques are involved? What partial progress has been made? Or do most people consider the effort/reward ratio of such an endeavor to be too high?

I think it would be interesting to have an algebraic proof, even a very long one, particularly if the algebraic proof does not use computers. Given its connection to many other areas (Temperley-Lieb Algebras), the problem seems to be amenable to other forms of attack.

4-colour Theorem. Every planar graph is 4-colourable.

This theorem of course has a well-known history. It was first proven by Appel and Haken in 1976, but their proof was met with skepticism because it heavily relied on the use of computers. The situation was partially remedied 20 years later, when Robertson, Sanders, Seymour, and Thomas published a new proof of the theorem. This new proof still relied on computer analysis, but to such a lower extent that their proof was actually verifiable. Finally, in 2005, Gonthier and Werner used the Coq proof assistant to formalize a proof, so I suppose only the most die hard skeptics remain.

My question stems from reading this paper by Robin Thomas. In it, he describes several interesting reformulations of the 4-colour theorem. Here is one:

Note that the cross-product on vectors in $\mathbb{R}^3$ is not an associative operation. We therefore define a bracketing of a cross-product $v_1 \times \dots v_n$ to be a set of brackets which makes the product well-defined.

Theorem. Let $i, j, k$ be the standard unit vectors in $\mathbb{R}^3$. For any two different bracketings of the product $v_1 \times \dots \times v_n$, there is an assignment of $i,j,k$ to $v_1, \dots, v_n$ such that the two products are equal and non-zero.

The surprising fact is that this innocent looking theorem implies the 4-colour theorem.

Question. Is anyone working on an algebraic proof of the 4-colour theorem (say by trying to prove the above theorem)? If so, what techniques are involved? What partial progress has been made? Or do most people consider the effort/reward ratio of such an endeavor to be too high?

I think it would be interesting to have an algebraic proof, even a very long one, particularly if the algebraic proof does not use computers. Given its connection to many other areas (Temperley-Lieb Algebras), the problem seems to be amenable to other forms of attack.

4-Colour Theorem. Every planar graph is 4-colourable.

This theorem of course has a well-known history. It was first proven by Appel and Haken in 1976, but their proof was met with skepticism because it heavily relied on the use of computers. The situation was partially remedied 20 years later, when Robertson, Sanders, Seymour, and Thomas published a new proof of the theorem. This new proof still relied on computer analysis, but to such a lower extent that their proof was actually verifiable. Finally, in 2005, Gonthier and Werner used the Coq proof assistant to formalize a proof, so I suppose only the most die hard skeptics remain.

My question stems from reading this paper by Robin Thomas. In it, he describes several interesting reformulations of the 4-colour theorem. Here is one:

Note that the cross-product on vectors in $\mathbb{R}^3$ is not an associative operation. We therefore define a bracketing of a cross-product $v_1 \times \dots v_n$ to be a set of brackets which makes the product well-defined.

Theorem. Let $i, j, k$ be the standard unit vectors in $\mathbb{R}^3$. For any two different bracketings of the product $v_1 \times \dots \times v_n$, there is an assignment of $i,j,k$ to $v_1, \dots, v_n$ such that the two products are equal and non-zero.

The surprising fact is that this innocent looking theorem implies the 4-colour theorem.

Question. Is anyone working on an algebraic proof of the 4-colour theorem (say by trying to prove the above theorem)? If so, what techniques are involved? What partial progress has been made? Or do most people consider the effort/reward ratio of such an endeavor to be too high?

I think it would be interesting to have an algebraic proof, even a very long one, particularly if the algebraic proof does not use computers. Given its connection to many other areas (Temperley-Lieb Algebras), the problem seems to be amenable to other forms of attack.

4-colour Theorem. Every planar graph is 4-colourable.

This theorem of course has a well-known history. It was first proven by Appel and Haken in 1976, but their proof was met with skepticism because it heavily relied on the use of computers. The situation was partially remedied 20 years later, when Robertson, Sanders, Seymour, and Thomas published a new proof of the theorem. This new proof still relied on computer analysis, but to such a lower extent that their proof was actually verifiable. Finally, in 2005, Gonthier and Werner used the Coq proof assistant to formalize a proof, so I suppose only the most die hard skeptics remain.

My question stems from reading this paper by Robin Thomas. In it, he describes several interesting reformulations of the 4-colour theorem. Here is one:

Note that the cross-product on vectors in $\mathbb{R}^3$ is not an associative operation. We therefore define a bracketing of a cross-product $v_1 \times \dots v_n$ to be a set of brackets which makes the product well-defined.

Theorem. Let $i, j, k$ be the standard unit vectors in $\mathbb{R}^3$. For any two different bracketings of the product $v_1 \times \dots \times v_n$, there is an assignment of $i,j,k$ to $v_1, \dots, v_n$ such that the two products are equal and non-zero.

The surprising fact is that this innocent looking theorem implies the 4-colour theorem.

Question. Is anyone working on an algebraic proof of the 4-colour theorem (say by trying to prove the above theorem)? If so, what techniques are involved? What partial progress has been made? Or do most people consider the effort/reward ratio of such an endeavor to be too high?

I think it would be interesting to have an algebraic proof, even a very long one, particularly if the algebraic proof does not use computers. Given its connection to many other areas (Temperley-Lieb Algebras), the problem seems to be amenable to other forms of attack.