Currently, there does not exist a manipulation of algebraic symbols to obtain any formal proof of the Four Color Theorem.

Proofs of the Four Color problem are most directly related
with the history of Proof Without Words. ( search this site )

Four Color theorem 'proofs' are diagrams. If we see enough cases in which something is true and we never see a case in which it is false, we tend to conclude that it is always true. This type of reasoning by example is called inductive reasoning. Inductive reasoning is not considered proof within formal logic.

Deductive reasoning is the only one that guarantees its conclusions.

Please, do explain the proof. Preferably in colour.

However, it'seems that, even though it is not an algebraic proof, there really will never be a counter-example and such dreams of finding new ways of mapping (or of new worlds to map) are come to nought.

In the absence of any real need for five colors, the hunt for a rigorous demonstrable proof is itself the hunt for new mathematical worlds, in which proof without words is not sufficient.

When the proof came out in the 70's, there was a lot of excitement, and many felt that computerized proofs of mathematics theorems were the wave of the future.

Simply put, that hasn't happened. Math journals are still pretty much the same as they were in the 70's, or even before the advent of the modern computer. What has changed is at the level of experimentation: a mathmatician nowadays will try to check what he or she believes to be true with as many computer generated examples as possible, before going for the full-blown mathematical proof.

And it turns out in the end not to be a very important problem. More interesting is the following: given a general graph (not necessarily planar), what is the minimum number of colors needed to color it? This problem is NP hard, and will get you a cool million from the Clay institute if you find a polynomial time algorithm that answers the question.