Computers and mathematical demonstrations

[ryokan]

I was impressed by the work of A. Wiles on the last Fermat's theorem, with the demonstration of the Taniyama-Shimura conjecture.

On the other hand, I think it is very interesting the demonstration of the four colours theorem by means of a lot of computer's work.

It seems to me that these two examples are very different forms of mathematic methodology.

What would be the future of "demonstration" by computer? Would it be a true demonstration? I am thinking in the potential power of genetic algorithms in this respect.

 

[arildno]

I think there will always be a lot to be proved analytically prior to accepting the validity of a "computer proof":
Typically, as in the 4-colour theorem, you'll need to prove that there is a finite number of cases involved, and that the proposed algorithm necessarily will check every case.

Possibly, there might exist other types of problems in which the validity of a "computer proof" is proven analytically beyond doubt , but I don't know of any such types as yet.

 

[Hurkyl]

Take as an example computer algebra systems. Mathematica and Magma outputs are already (somewhat) accepted as proofs... for example, IIRC, the current best algorithm for computing digits of pi (in base 16) was proved using mathematica.

http://mathworld.wolfram.com/BBPFormula.html

 

[ryokan]

Thank you arildno and Hurkyl.
Then it is conceivable that development of some mathematical areas be linked, in a dependent form, to the development of software?Or in simplistic terms: whithout computers, no more advances in a mathematical region ?

Other question: what is the actual role of genetic algorithms as aid to Math ?